lcp [Thu, 06 Apr 1995 11:55:51 +0200] rev 1010
Added comment.
lcp [Thu, 06 Apr 1995 11:14:51 +0200] rev 1009
No longer builds the induction structure (from ../Provers/ind.ML)
lcp [Thu, 06 Apr 1995 11:12:35 +0200] rev 1008
Loads the local hypsubst.ML. No longer loads ../Provers/ind.ML,
which was never used.
lcp [Thu, 06 Apr 1995 11:09:15 +0200] rev 1007
Corrected many errors in the dependencies.
lcp [Thu, 06 Apr 1995 11:07:18 +0200] rev 1006
Changed comments and timings.
lcp [Thu, 06 Apr 1995 11:04:37 +0200] rev 1005
Updated comments.
lcp [Thu, 06 Apr 1995 11:02:55 +0200] rev 1004
Set up for new hyp_subst_tac.
lcp [Thu, 06 Apr 1995 11:01:13 +0200] rev 1003
Added Id: line
lcp [Thu, 06 Apr 1995 10:58:56 +0200] rev 1002
Fixed typo.
lcp [Thu, 06 Apr 1995 10:56:39 +0200] rev 1001
Simplified some proofs and made them work for new hyp_subst_tac.
lcp [Thu, 06 Apr 1995 10:55:06 +0200] rev 1000
Now sets loadpath.
lcp [Thu, 06 Apr 1995 10:53:21 +0200] rev 999
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp [Thu, 06 Apr 1995 10:51:42 +0200] rev 998
Gave tighter priorities to if, napply and the let-forms to
reduce ambiguities.
lcp [Thu, 06 Apr 1995 10:49:53 +0200] rev 997
Now sets eta_contract.
lcp [Thu, 06 Apr 1995 10:48:11 +0200] rev 996
Added Id: line
nipkow [Sun, 02 Apr 1995 10:43:59 +0200] rev 995
generalized map (%x.x) xs = xs to map (%x.x) = (%xs.xs)
wenzelm [Fri, 31 Mar 1995 15:08:49 +0200] rev 994
replaced 'arities' by 'instance';
lcp [Fri, 31 Mar 1995 12:22:16 +0200] rev 993
Simplified using pattern replacements. Added the AC example.
lcp [Fri, 31 Mar 1995 11:55:29 +0200] rev 992
New example of AC Equivalences by Krzysztof Grabczewski
lcp [Fri, 31 Mar 1995 11:39:47 +0200] rev 991
New example of AC Equivalences by Krzysztof Grabczewski
lcp [Fri, 31 Mar 1995 11:08:35 +0200] rev 990
Tried the new addss in many proofs, and tidied others involving simplification.
lcp [Fri, 31 Mar 1995 10:58:14 +0200] rev 989
Tried the new addss in a proof.
lcp [Fri, 31 Mar 1995 02:00:29 +0200] rev 988
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 14:07:52 +0200] rev 987
changed translation of _applC
clasohm [Thu, 30 Mar 1995 14:07:30 +0200] rev 986
changed pretty printing of applC
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)