Adapting the HOL88 tutorial to HOL90
Rather than try to redo the entire tutorial, this page merely lists
the HOL90 format for commands in portions of the HOL88 tutorial, along
with a few general notes.
General Notes
(thanks to Andreas Graubner for adding to these notes)
- The HOL90 prompt is - instead of #.
- The prompt changes to = if you have not entered a complete expression.
- Commands should be followed by ; instead of ;;
- To assign a non-function value to a variable, use val instead of
let. If let is used to define a function, replace it with fun.
- The syntax for a term is (--`term`--) (those should be backquotes,
even if they appear as quotes in Mosaic).
- Exit the system by typing Control-d in the shell or by C-q C-d
in gnuemacs.
- Knowing a little SML/NJ will make
learning HOL90 from the classic HOL documentation even easier.
- exit(); will terminate hol90, and can be used to do so in scripts.
- remarks have the form '(*...*)' in HOl90 (instead of '%...' in HOL88)
- list separator is ',' in HOL90 (instead of ';' in HOL88)
- lambda operator is 'fn' in HOL90 (instead of '\' in HOL88)
- some HOL88 functions are not implemented in HOL90 (e.g. 'words' -> use
'words2', 'new_prim_rec_definition' -> use 'new_recursive_definition')
- do not use 'in' as a variable name (e.g. in --`!in. in = 0`--) because
HOL90 gets confused
- some functions do not return pairs like `Y * `Z as in HOL88, they changed
it to parameters like {Bvar:term, Body:term}
This set of notes
for chapter three was provided by Thirunarayan Krishnaprasad.
The general hints above plus the notes
should get you through most of chapter 4 in HOL90.
Most of the chapter 5 tutorial works without modifications other than
those cited in the general notes above.
Andreas Graubner provided notes for
the parity checker example.