Encoding forall ``\x P(x) = \x true` is saying that the predictae p is always true.
- Harrison’s page
- tutorial quite good
- Thomas Hale - Formal Proof article Succinct summary of axioms
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?
Sledgehammer: some history, some tips isabelle cookboook: programming in ML more isabelle ML programming notes
Isabelle => vs –> vs ==> => is the function type –> is implication ==> is meta implication, which is something like a sequent |-