Lines Matching defs:library
3 This document describes the facilities provided by the \ml{unwind} library
4 for the HOL system~\cite{description}. The library provides conversions and
30 \section{Using the library}
32 The \ml{unwind} library can be loaded into a \HOL\ session using the function
34 manual for a general description of library loading). The first action in the
38 library. After updating the help search path, the \ML\ functions in the
39 library are loaded into \HOL.
41 The following session shows how the \ml{unwind} library may be loaded using
47 Loading library `unwind` ...
54 We now illustrate the use of the library on the parity-checker example.
160 which lines to unwind. The tools in the \ml{unwind} library allow the user