lcp [Thu, 30 Mar 1995 14:01:35 +0200] rev 985
Added comment about why mem_irrefl should not be a safeE.
lcp [Thu, 30 Mar 1995 13:54:41 +0200] rev 984
Tried the new addss in many proofs, and tidied others
involving simplification.
lcp [Thu, 30 Mar 1995 13:48:30 +0200] rev 983
Precedence of infixes is now 4 (just above that of :=)
lcp [Thu, 30 Mar 1995 13:44:34 +0200] rev 982
Addition of wrappers for integration with the simplifier.
New infixes setwrapper compwrapper addbefore addafter. New function
getwrapper. The wrapper is a tactical that is applied to the step tactic. By
default it is the identity. Using THEN one can cause other tactics to be
tried before or after the step tactic. Other effects are possible using
ORELSE, etc.
lcp [Thu, 30 Mar 1995 13:36:00 +0200] rev 981
Defined addss to perform simplification in a claset.
Precedence of addcongs is now 4 (to match that of other simplifier infixes)
clasohm [Thu, 30 Mar 1995 13:07:59 +0200] rev 980
removed unnecessary parentheses from the generated rules
nipkow [Thu, 30 Mar 1995 08:54:17 +0200] rev 979
Simplification: used Logic.occs instead of mem add_term_frees
clasohm [Tue, 28 Mar 1995 13:13:17 +0200] rev 978
changed string scanner so that newlines ('\n') are allowed and ignored inside
strings
clasohm [Tue, 28 Mar 1995 12:25:20 +0200] rev 977
changed syntax of datatype declarations (curried types for constructor
parameters)
clasohm [Tue, 28 Mar 1995 12:21:10 +0200] rev 976
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
apfst from Pure/library.ML