1996-06-06 paulson [Thu, 06 Jun 1996 13:13:18 +0200] rev 1788
Quotes now optional around inductive set
src/HOL/Sexp.thy src/HOL/thy_syntax.ML

1996-06-04 paulson [Tue, 04 Jun 1996 12:49:04 +0200] rev 1787
Tidied some proofs
src/ZF/Perm.ML

1996-06-03 berghofe [Mon, 03 Jun 1996 17:10:56 +0200] rev 1786
best_tac, deepen_tac and safe_tac now also use default claset.
src/HOL/Arith.ML src/HOL/Finite.ML src/HOL/Nat.ML src/HOL/Relation.ML src/HOL/Trancl.ML src/HOL/Univ.ML src/HOL/WF.ML src/HOL/equalities.ML

1996-06-03 paulson [Mon, 03 Jun 1996 11:44:44 +0200] rev 1785
Shortened some proofs
src/ZF/ex/Ramsey.ML

1996-06-03 paulson [Mon, 03 Jun 1996 11:43:55 +0200] rev 1784
Added a new theorem, UN_Int_subset
src/ZF/equalities.ML

1996-06-03 paulson [Mon, 03 Jun 1996 11:41:26 +0200] rev 1783
Used 2 instead of Suc(Suc 0)
src/HOL/ex/NatSum.ML

1996-06-03 paulson [Mon, 03 Jun 1996 11:41:00 +0200] rev 1782
Shortened a proof
src/HOL/Finite.ML src/ZF/Perm.ML src/ZF/ex/misc.ML

1996-05-31 oheimb [Fri, 31 May 1996 20:25:59 +0200] rev 1781
adapted use of monofun_cfun_arg
src/HOLCF/domain/theorems.ML

1996-05-31 oheimb [Fri, 31 May 1996 20:14:42 +0200] rev 1780
adapted proof of flat_codom
src/HOLCF/Fix.ML

1996-05-31 oheimb [Fri, 31 May 1996 19:55:19 +0200] rev 1779
introduced forgotten bind_thm calls
src/HOLCF/Cfun2.ML src/HOLCF/Cfun3.ML src/HOLCF/Cont.ML src/HOLCF/Cprod2.ML src/HOLCF/Cprod3.ML src/HOLCF/Fix.ML src/HOLCF/Fun2.ML src/HOLCF/Lift2.ML src/HOLCF/Pcpo.ML src/HOLCF/Porder.ML src/HOLCF/ROOT.ML src/HOLCF/Sprod2.ML src/HOLCF/Sprod3.ML src/HOLCF/Ssum2.ML