1996-05-23 berghofe [Thu, 23 May 1996 15:15:20 +0200] rev 1761
Removed equalityI from some proofs (because it is now included
in the default claset)
src/HOL/Relation.ML src/HOL/Sum.ML src/HOL/Univ.ML src/HOL/subset.ML

1996-05-23 berghofe [Thu, 23 May 1996 14:37:06 +0200] rev 1760
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
src/HOL/Arith.ML src/HOL/Finite.ML src/HOL/Lfp.ML src/HOL/List.ML src/HOL/Nat.ML src/HOL/RelPow.ML src/HOL/Set.ML src/HOL/Sexp.ML src/HOL/Sum.ML src/HOL/Trancl.ML src/HOL/Univ.ML src/HOL/WF.ML src/HOL/mono.ML src/HOL/subset.ML

1996-05-22 nipkow [Wed, 22 May 1996 18:32:37 +0200] rev 1759
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
src/HOL/Lambda/Eta.ML src/HOL/Lambda/Lambda.ML

1996-05-22 nipkow [Wed, 22 May 1996 17:30:16 +0200] rev 1758
Added ex_imp
src/HOL/simpdata.ML

1996-05-22 nipkow [Wed, 22 May 1996 17:11:54 +0200] rev 1757
Added the second half of the W/I correspondence.
src/HOL/MiniML/I.ML src/HOL/MiniML/Maybe.ML

1996-05-22 nipkow [Wed, 22 May 1996 16:54:16 +0200] rev 1756
Added swap_prems_rl
src/Pure/drule.ML

1996-05-21 berghofe [Tue, 21 May 1996 13:42:53 +0200] rev 1755
Added additional parent theory equalities because some proofs in
Prod.ML depend on rules proved in equalities.ML
src/HOL/Prod.thy

1996-05-21 berghofe [Tue, 21 May 1996 13:39:31 +0200] rev 1754
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
src/HOL/Fun.ML src/HOL/Prod.ML src/HOL/Relation.ML src/HOL/equalities.ML

1996-05-21 nipkow [Tue, 21 May 1996 10:52:26 +0200] rev 1753
Corrected comment wrt I
src/HOL/MiniML/README.html

1996-05-21 nipkow [Tue, 21 May 1996 10:50:40 +0200] rev 1752
Updated url.
src/HOL/MiniML/README.html