Thu, 30 Mar 1995 13:44:34 +0200 Addition of wrappers for integration with the simplifier.
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.
Thu, 30 Mar 1995 13:36:00 +0200 Defined addss to perform simplification in a claset.
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)
Thu, 30 Mar 1995 13:07:59 +0200 removed unnecessary parentheses from the generated rules
clasohm [Thu, 30 Mar 1995 13:07:59 +0200] rev 980
removed unnecessary parentheses from the generated rules
Thu, 30 Mar 1995 08:54:17 +0200 Simplification: used Logic.occs instead of mem add_term_frees
nipkow [Thu, 30 Mar 1995 08:54:17 +0200] rev 979
Simplification: used Logic.occs instead of mem add_term_frees
Tue, 28 Mar 1995 13:13:17 +0200 changed string scanner so that newlines ('\n') are allowed and ignored inside
clasohm [Tue, 28 Mar 1995 13:13:17 +0200] rev 978
changed string scanner so that newlines ('\n') are allowed and ignored inside strings
Tue, 28 Mar 1995 12:25:20 +0200 changed syntax of datatype declarations (curried types for constructor
clasohm [Tue, 28 Mar 1995 12:25:20 +0200] rev 977
changed syntax of datatype declarations (curried types for constructor parameters)
Tue, 28 Mar 1995 12:21:10 +0200 renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
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
Tue, 28 Mar 1995 10:24:45 +0200 Corrected faulty reference to Hindley-Milner type inference
lcp [Tue, 28 Mar 1995 10:24:45 +0200] rev 975
Corrected faulty reference to Hindley-Milner type inference
Mon, 27 Mar 1995 18:29:23 +0200 Added recursion equations for foldl to list_ss.
nipkow [Mon, 27 Mar 1995 18:29:23 +0200] rev 974
Added recursion equations for foldl to list_ss.
Sun, 26 Mar 1995 17:04:45 +0200 Modified If_def to avoid ambiguity.
nipkow [Sun, 26 Mar 1995 17:04:45 +0200] rev 973
Modified If_def to avoid ambiguity.
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip