Encoding forall ``\x P(x) = \x true` is saying that the predictae p is always true.


  • cakeml a verified implementation of an ML in HOL4
  • holpy


HOL light


from lcf to isabelle sel4 - verified microkernel

Metalevel is a syntax for describing inference rules

  • !! x. \Lambda Universal variables at the meta level. enables Schema
  • ==> is inference rule
  • %x. is meta level lambda?

typeclasses vs locales

Sledgehammer: some history, some tips isabelle cookboook: programming in ML more isabelle ML programming notes

Baby examples

Isabelle => vs –> vs ==> => is the function type –> is implication ==> is meta implication, which is something like a sequent |-