README
1+ ===================================================================== +
2| |
3| LIBRARY : simp |
4| |
5| DESCRIPTION : A conditional/contextual Isabelle-style simplifier. |
6| |
7| AUTHOR : D.R.Syme |
8| DATE : 1996 |
9| |
10| MODIFIED : R.J.Boulton |
11| DATE : 6 August 1996 |
12+ ===================================================================== +
13
14A conditional/contextual Isabelle-style simplifier, with additional
15integration of the "ARITH" decision procedure for natural numbers.
16There is some documentation in doc/simp.tex. Some test code is included in
17src/test.sml.
18
19Structures: Simplifier, Simpsets, arith_ss, Trace, Theorems and others
20
21Important functions:
22 Tactics: SIMP_TAC, ASM_SIMP_TAC, FULL_SIMP_TAC
23 Making simpsets: rewrites, mk_simpset , see examples in src/Simpsets.sml
24 Tracing: trace_level := ...
25
26