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