Notes for HOL90 Beginners

Having started to learn HOL90 without the aid of a HOL90 specific manual, I've put together this page in hopes of helping other beginners over the early hurdles that I encountered in trying to learn to use the system. This is in no way intended to be a full tutorial for HOL90; it is basically a reference page for the things I`ve needed to know so far in order to start seriously playing with HOL90. Send any corrections or suggestions about these notes (including other personal notes that might be helpful to beginners) to me (Kathi Fisler) at and I'll add them to the page. (I may also try to keep them updated as I learn more, but I don't make any promises on that front.)

The HOL Documentation System

Presumably, if you found this page you have also found the on-line documentation system for HOL. The information here is quite thorough, with it's only drawback being that it is written for HOL88 as opposed to HOL90. I've put together a series of notes for adapting the existing on-line tutorial to HOL90. I found that most of the existing documentation is easily usable in HOL90 once you've figured out a few syntactic differences. Most of the rest of this page will make no sense unless you've done the tutorial or had some prior experience with the system.


HOL90 is implemented on top of SML/NJ, so knowing some of that system helps.

Help for Error Messages

If you get a HOL_ERROR from typing "exp;", typing "exp handle e => Raise e;" usually returns a more detailed error message.

Interactive versus Non-interactive Proof

The distribution files are a good source for sample proofs and definitions (I've also provided a very easy theory definition with some proofs below), but there are some minor tricks that might help you use the system interactively.

It helps tremendously to run HOL90 inside of Emacs. You can either refer to the information on this in the HOL documentation, or you can simply run HOL90 within a shell running inside of Emacs. I've found it very helpful to use a large Emacs screen, split it in two (C-x 2), and run HOL90 in one half while editing an Emacs file with the theory I'm trying to write in the other half. This allows me to construct a non-interactive proof in the file as I find the steps work in the interactive proof. I've yet to find a built-in way to save the steps taken in an interactive proof.

I've found two ways to use steps saved in a file on an interactive proof. One is to cut and paste steps from the file into an e( ) at the HOL90 prompt (this is one reason why running in emacs is a great help). The other is to just cut and paste the steps into the session without the e( ). If you do the latter, the variable "it" now contains a tactic that performs the series of pasted steps. This tactic can be applied by typing

 e it; 
at the prompt. I find this is sometimes helpful in debugging the syntax of the commands without affecting the goalstack history.

Learning the HOL style of proof

Once you understand the syntactic differences between HOL90 and classic HOL, the on-line documentation can be used easily for learning how proofs work in the system. Read the HOL description manual for information on tactics, conversions, rewriting, and anything else you need to know to get started.

Miscellaneous Notes

This is a random collection of things that I have picked up or needed to know while learning the system.

If all else fails ...

and you are UNIX literate, grepping the source files can be very helpful. Look in src/[0,1,2,3]/* in the distribution.

The people on info-hol are also very helpful if you have questions. Send mail to to join the mailing list.

A Sample Proof