All 28 Packages
- axiom — Standard axioms
- base — The standard theory library
- bool — Boolean operators and quantifiers
- byte — Bytes
- char — Unicode characters
- cl — Combinatory logic example illustrating inductive definitions in HOL4
- empty — The empty theory
- function — Function operators and combinators
- gfp — Parametric theory of GF(p) finite fields
- lazy-list — Lazy lists/colists/streams
- list — List types
- modular — Parametric theory of modular arithmetic
- natural — The natural numbers
- natural-divides — The divides relation on natural numbers
- natural-gcd — Natural number greatest common divisor
- natural-prime — Prime natural numbers
- option — Option types
- pair — Product types
- parser — Stream parsers
- real — The real numbers
- relation — Relation operators
- set — Set types
- sum — Sum types
- unit — The unit type
- word — Parametric theory of words
- word10 — 10-bit words
- word12 — 12-bit words
- word16 — 16-bit words