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.

- The backup(); command demonstrated in the tutorial can be
abbreviated as b();
- Sometimes you need to add typing information when trying to
discharge assumptions, even if that information is not displayed in
the assumption. For example, in the following proof fragment, I want
to discharge (--`x t`--), where x is a function from num to bool.
____________________________ (--`x t`--) (--`y t`--) : goalstack - e(UNDISCH_TAC (--`x t`--)); Unconstrained type variable in the variable (x :?2 -> ?3) Exception raised at Preterm.typecheck_cleanup: uncaught exception HOL_ERR -

If the command is given as

e(UNDISCH_TAC (--`(x:num->bool) t`--));

it will discharge without error. - If you are working interactively and have made enough errors that
the goal stack is no longer visible on the screen, typing
e(ALL_TAC);

will bring up the current goal stack without changing it. I've been told that the stack history (what you can undo with backup) is limited to 15 steps, so after the ALL_TAC you might want to backup once, to avoid leaving the ALL_TAC in the goal history. - When rewriting, HOL90 rewrites the left side of a theorem with
the right. If you need to rewrite the right side with the left, you
have to manually switch the right and left hand sides using the GSYM
command before trying to rewrite.
- ADD_SUC; val it = |- !m n. SUC (m + n) = m + SUC n : thm - GSYM(ADD_SUC); val it = |- !m n. m + SUC n = SUC (m + n) : thm

- You can apply a conversion as a tactic by applying CONV_TAC to
the conversion.
- Certain single-letter variable names are reserved as combinators
in the language, and are not available for use in your own
definitions. I ran into this problem trying to use the letter o to
define a function from num->bool. I don't know the full list of such
letters, but be aware of the problem.
- Rewriting can sometimes go into an infinite loop if you have a formula that rewrites to something that can itself be rewritten. Using ONCE_REWRITE_TAC (or ONCE_ASM_REWRITE_TAC if you are rewriting with the assumptions) will avoid this problem.

The people on info-hol are also very helpful if you have questions. Send mail to info-hol-request@lal.cs.byu.edu to join the mailing list.