# HOL

# Axioms

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

# HOL

HOL4 https://kth-step.github.io/itppv-course/

# HOL light

- wikpedia
- Harrison’s page
- tutorial quite good
- Thomas Hale - Formal Proof article Succinct summary of axioms
- #

# Isabelle

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 |-