Keyboard shortcuts

Enter	Submit code
Shift+Enter	Newline
↑ / ↓	Browse history
Ctrl+L	Clear output
Ctrl+K	Reset toplevel

Examples

• A simple term
• Prove with ARITH_TAC
• Goal stack: existential
• Propositional tautology
• A nonlinear arithmetic identity
• Sum 1..n by induction
• loadt + coprime test
• Distributivity of bit-vector add and mul
• Define a constant
• Recursive function: Fibonacci
• Define a new type: binary tree
• help

References

• Reference Manual
• HOL Light Tutorial

Heads up

There is no interrupt in this interface — a runaway proof (e.g. a non-terminating REWRITE_CONV) cannot be cancelled. Ctrl+K wipes the toplevel and re-boots the kernel from scratch (~1–2 min), so use it only as a last resort.

The search command is not available here: update_database.ml is intentionally not shipped with this build (so loadt "update_database.ml";; will fail with a file-not-found).