15 \end{flushright} |
15 \end{flushright} |
16 |
16 |
17 \medskip |
17 \medskip |
18 HOL is based on just a few primitive constants, like equality and |
18 HOL is based on just a few primitive constants, like equality and |
19 implication, whose properties are described by axioms. All other concepts, |
19 implication, whose properties are described by axioms. All other concepts, |
20 such as inductive predicates, datatypes, or recursive functions are defined |
20 such as inductive predicates, datatypes, or recursive functions have to be defined |
21 in terms of those constants, and the desired properties, for example |
21 in terms of those constants, and the desired properties, for example |
22 induction theorems, or recursion equations are derived from the definitions |
22 induction theorems, or recursion equations have to be derived from the definitions |
23 by a formal proof. Since it would be very tedious for a user to define |
23 by a formal proof. Since it would be very tedious for a user to define |
24 complex inductive predicates or datatypes ``by hand'' just using the |
24 complex inductive predicates or datatypes ``by hand'' just using the |
25 primitive operators of higher order logic, \emph{definitional packages} have |
25 primitive operators of higher order logic, \emph{definitional packages} have |
26 been implemented automating such work. Thanks to those packages, the user |
26 been implemented automating such work. Thanks to those packages, the user |
27 can give a high-level specification, for example a list of introduction |
27 can give a high-level specification, for example a list of introduction |