1996-04-22 nipkow [Mon, 22 Apr 1996 15:42:20 +0200] rev 1669
inserted Suc_less_eq explictly in a few proofs.
inserted o_def explictly in a few proofs because the new split_tac causes
fewer eta-expansions which some of the rewrites need.

Indented proof in I.ML
src/HOL/MiniML/I.ML src/HOL/MiniML/W.ML

1996-04-19 clasohm [Fri, 19 Apr 1996 11:33:24 +0200] rev 1668
added Konrad's code for the datatype package
src/HOL/HOL.ML src/HOL/datatype.ML src/HOL/thy_data.ML src/HOL/thy_syntax.ML

1996-04-19 clasohm [Fri, 19 Apr 1996 11:18:59 +0200] rev 1667
adapted to new version of Fun.ML
src/HOL/IOA/ABP/Correctness.ML src/HOL/IOA/meta_theory/Solve.ML

1996-04-19 clasohm [Fri, 19 Apr 1996 11:13:05 +0200] rev 1666
removed assignment of HOL_ss to simpset
src/HOL/Fun.ML

1996-04-19 clasohm [Fri, 19 Apr 1996 11:12:05 +0200] rev 1665
added thy_data.ML
src/HOL/Makefile

1996-04-19 clasohm [Fri, 19 Apr 1996 11:10:26 +0200] rev 1664
added thyname_of_sign (used in HOL/thy_data.ML)
src/Pure/Thy/thy_read.ML

1996-04-18 oheimb [Thu, 18 Apr 1996 14:43:00 +0200] rev 1663
adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
src/ZF/List.ML

1996-04-18 oheimb [Thu, 18 Apr 1996 14:11:02 +0200] rev 1662
adapted proof of less_succ: problem because of non-confluent SimpSet removed
src/FOL/ex/Nat2.ML

1996-04-18 oheimb [Thu, 18 Apr 1996 12:33:05 +0200] rev 1661
*** empty log message ***
src/FOL/ex/Nat2.ML

1996-04-17 oheimb [Wed, 17 Apr 1996 17:59:58 +0200] rev 1660
*** empty log message ***
src/HOL/Arith.ML src/HOL/Finite.ML src/HOL/HOL.ML src/HOL/Nat.ML src/HOL/Nat.thy src/HOL/Prod.thy src/HOL/equalities.ML src/HOL/simpdata.ML