Adapting the HOL88 tutorial to HOL90

(This is a local adaptation, for teaching purposes, of http://www.cs.indiana.edu/hyplan/kfisler/HOL/holtutnotes.html)

General 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}

Tutorial Chapter 3

Tutorial Chapter 4

Tutorial Chapter 5

Tutorial Chapter 6