Wrap module and open declarations with a compiler directive so they're not used when running in scripting mode (i.e., F# interactive). This is to emulate the way hol-light loads code into the OCaml toplevel.
Added hol.bat script to load up an FSI session with all of our code, just as in hol-light.
Renamed system.fs to system.fsx; moved code from Tutorial/init.fsx into it.
Moved Tutorial/hol.bat into the solution's root folder.
Added additional information to the exception raised when TAC_PROOF fails.
Merge branch 'no-interactive-modules'.