All 54 Packages
- arm-decomp — ARM decompilation support
- arm-model — ARM model
- arm-prog — ARM evaluator
- arm-step — ARM step evaluator
- 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
- hol-base — HOL basic theories
- hol-floating-point — HOL floating point theories
- hol-integer — HOL integer theories
- hol-monad — HOL monad theories
- hol-quotient — HOL quotient theories
- hol-real — HOL real theories
- hol-res-quan — HOL theory about restricted quantifiers
- hol-ring — HOL ring theories
- hol-sort — HOL sorting theories
- hol-string — HOL string theories
- hol-words — n-bit words
- lazy-list — Lazy lists/colists/streams
- list — List types
- m0-decomp — M0 decompilation support
- m0-model — M0 model
- m0-prog — M0 evaluator
- m0-step — M0 step evaluator
- machine-code-hoare-logic — A Hoare logic for machine code
- machine-code-hoare-logic-state — Machine code Hoare logic state
- machine-code-hoare-triple — Total correctness machine-code Hoare triple
- machine-code-straightline — Hoare logic triple support for straightline code
- modular — Parametric theory of modular arithmetic
- natural — The natural numbers
- natural-bits — Natural number to bit-list conversions
- natural-divides — The divides relation on natural numbers
- natural-fibonacci — Fibonacci numbers
- natural-prime — Prime natural numbers
- option — Option types
- pair — Product types
- parser — Stream parsers
- probability — Probability
- real — The real numbers
- relation — Relation operators
- set — Set types
- stream — Infinite stream 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
Gilith OpenTheory Repo, maintained by