Lines Matching defs:The
1 \chapter{The reduce Library}
4 its design. The library is intended to ease the burden of performing tedious
19 primitive inferences than a human would take. The library will also take care
24 \section{The representation of numbers}
26 The approach to representing natural number constants in \HOL\ is to provide a
42 The \ml{reduce} library uses only the above conversion, together with certain
50 The following is an example of an algorithm for reducing addition expressions.
84 This gives the desired result. The above can easily be converted into a
91 The straightforward way to use the library is simply to do:
101 The library provides the following three ML bindings, which should be all that
130 these, refer to the next chapter. The arithmetic conversions and boolean