src/ZF/AC/AC2_AC6.ML
Tue, 04 Mar 1997 10:42:28 +0100 paulson best_tac avoids looping with change to RepFun_eqI in claset
Thu, 09 Jan 1997 10:20:03 +0100 paulson Removal of needless "addIs [equality]", etc.
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Wed, 21 Aug 1996 11:43:37 +0200 paulson Tidying: removing redundant args in classical reasoner calls
Tue, 20 Aug 1996 12:23:13 +0200 paulson Corrected for new classical reasoner: redundant rules
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 28 Jul 1995 11:48:55 +0200 lcp Ran expandshort and changed spelling of Grabczewski
Tue, 25 Jul 1995 17:31:53 +0200 lcp Numerous small improvements by KG and LCP
Thu, 18 May 1995 11:51:23 +0200 lcp Krzysztof Grabczewski's (nearly) complete AC proofs
less more (0) tip