IT/Description/version2.tex

6 This appendix summarizes the differences between \HOL 88 Version 2.0
17 The top-level directory of the \HOL\ distribution sources has been
19 Installing \HOL').  An important addition is a directory
20 {\small\verb%contrib%} containing contributions from the \HOL\ user
48 Four libraries from Version 1.11 of HOL have been temporarily withdrawn,
110 of methodologies for embedding application-specific languages in \HOL\
114 quotation typecheckers for the \HOL\ logic. This enables more type
128 The top-level of the \HOL\ distribution directory now contains:
151 the \HOL\ distribution directory (`\ml{hol}') resides.
180 \noindent returns the internal pathname used by \HOL\ to
182 value when the system is built, should be the absolute pathname of the \HOL\
189 \noindent where $directory$ is the site-specific absolute pathname in which the \HOL\
194 library load-files to update the \HOL\ search path and help search
259 internal search path used by \HOL\ to find online help files.  The help
267 \index{types, in HOL logic@types, in \HOL\ logic! dependent}
268 \index{dependent types in HOL logic@dependent types in \HOL\ logic}
271 provided. This follows a suggestion discussed at the Second \HOL\ Users
342 for each \HOL\ session (e.g. with a {\small\verb%hol-init.ml%} initialization file).
714 languages into \HOL\ terms. See the documentation of the library for
777 The typechecker for \HOL\ quotations contains a number of arbitrary
785 The \ML\ abstract type {\small\verb%preterm%} represents the parse trees of \HOL\
787 \ml{preterm} is set to \ml{true} (the default is \ml{false}), then \HOL\ will use
793 around the quotation.\index{type checking, in HOL logic@type checking,
794 in \HOL\ logic!user programmed} Other uses of preterms are possible, for example
816 \noindent invokes the standard \HOL\ typechecker on a preterm and returns the
855 not compromise the logical soundness of \HOL.
1003 \index{let-terms, in HOL logic@\ml{let}-terms, in \HOL\ logic!simplification of}
1229 Quite a few new theorems have been added to \HOL.  Some are listed
1359 \noindent The file \ml{Version.$m$.$n$} (in the sources) documents \HOL\
1429 cleaning'' of the \HOL\ sources. It is hoped that nothing in use has been