1996-04-23 oheimb [Tue, 23 Apr 1996 16:44:22 +0200] rev 1671
included (empty) test goal for symmetry reasons
src/Pure/Makefile

1996-04-23 clasohm [Tue, 23 Apr 1996 12:38:16 +0200] rev 1670
use_dir and exit_use_dir now change the CWD only temporarily
src/Pure/Thy/thy_read.ML

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