Dear Lockwood,
First, thank you for taking the time to try out HOL-Omega. You are a
pioneer!
Yes, you are correct in all you are reporting about the examples in the
HOL-Omega Tutorial, that they work correctly for interactive use, but will
fail when inserted directly, without modification, into a
I have had HOL Omega installed, asking that the instructions of Section 1.3 of
the HOL Omega System Tutorial be followed (what I am unfortunately too ignorant
to attempt myself), and have been working my way through the Tutorial with
great interest, Holmake-ing the example theories as I go. All
