File: theorems-intro.tex

package info (click to toggle)
hol88 2.02.19940316dfsg-8
  • links: PTS
  • area: main
  • in suites: forky, sid
  • size: 65,960 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (14 lines) | stat: -rw-r--r-- 613 bytes parent folder | download | duplicates (11)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
This chapter gives all the definitions and theorems in the
\ml{more\_arithmetic} library. The theorems are grouped into sections
according to subject matter. Some theorems could be classified under more than
one subject, but each theorem is listed in only one section. The reader may
therefore have to consult more than one section when searching for any
particular theorem.


 When the library is loaded, all the theorems in the library are set up to
autoload when their names are mentioned in \ML.  The name of the theory in
which each theorem is stored is given in parentheses after the name of the
theorem.