Filter
Top Products
104 APPENDIX A. COMPATIBILITY WITH OTHER HOLS
• The names of many theorems, especially about natural numbers, are different.
Some of the operations on natural numbers are defined differently.
• Various facilities are in the core system rather than loadable libraries, e.g. tau-
tology checking, higher order matching, first order reasoning, quotient types,
integers, reals and nested recursive types.
• The axiomatization of the logic is simpler and all ‘derived rules’ are genuinely
derived. There is no separate boolean cases axiom, since it follows from the
axiom of choice.
• The preferred concrete syntax for conditional expressions is ‘if . . .then . . .else
. .. ’, although the old HOL syntax is still accepted.
• The internal encodings of paired abstractions and let-terms are different. The
former is an instance of a more general method of allowing abstractions over
arbitrary expressions.
• The term syntax uses a name-carrying representation like HOL88, rather than
a de Bruijn representation as in hol90. It was felt that this would be more
efficient on average, even if it makes a couple of primitive term operations like
substitution tricky to get right.
Despite the above, readers familiar with older HOLs should find the system
reasonably familiar. Many of the differences do not greatly affect day-to-day use of
the system.