Lines Matching defs:library
3 This document describes the facilities provided by the \ml{arith} library
75 \section{Using the library}
77 The \ml{arith} library can be loaded into a user's \HOL\ session using the
79 \HOL\ manual for a general description of library loading). The first action
83 library. After updating the help search path, the \ml{reduce}
84 library~\cite{reduce} is loaded. The \ml{arith} library makes use of some of
85 the functions in the \ml{reduce} library. Finally, the \ML\ functions in the
86 \ml{arith} library are loaded into \HOL.
88 The following session shows how the \ml{arith} library may be loaded using
94 Loading library `arith` ...
96 .Loading library `reduce` ...