1998-10-21 berghofe [Wed, 21 Oct 1998 17:46:00 +0200] rev 5716
Changed syntax of rep_datatype and inductive: Theorems
are no longer specified by a string of ML type "thm list" but
by a comma-separated list of identifiers, which are looked
up in the theory.
src/HOL/thy_syntax.ML

1998-10-21 berghofe [Wed, 21 Oct 1998 17:40:35 +0200] rev 5715
Added theorem prod_induct (needed for rep_datatype).
src/HOL/Prod.ML

1998-10-21 berghofe [Wed, 21 Oct 1998 17:38:47 +0200] rev 5714
Changed syntax of rep_datatype.
src/HOL/Datatype.thy src/HOL/Nat.thy

1998-10-21 wenzelm [Wed, 21 Oct 1998 16:38:46 +0200] rev 5713
fixed field_injects;
src/HOL/Tools/record_package.ML

1998-10-21 wenzelm [Wed, 21 Oct 1998 16:34:18 +0200] rev 5712
tuned;
src/HOL/AxClasses/Lattice/Lattice.ML src/HOL/AxClasses/Lattice/OrdDefs.ML src/HOL/AxClasses/Lattice/ROOT.ML src/HOL/AxClasses/Lattice/tools.ML src/HOL/IsaMakefile

1998-10-21 wenzelm [Wed, 21 Oct 1998 16:06:09 +0200] rev 5711
no open;
src/HOL/AxClasses/Lattice/CLattice.ML src/HOL/AxClasses/Lattice/LatInsts.ML src/HOL/AxClasses/Lattice/LatMorph.ML src/HOL/AxClasses/Lattice/LatPreInsts.ML src/HOL/AxClasses/Lattice/Lattice.ML src/HOL/AxClasses/Lattice/OrdDefs.ML src/HOL/AxClasses/Lattice/Order.ML src/HOL/AxClasses/Tutorial/Group.ML

1998-10-21 wenzelm [Wed, 21 Oct 1998 16:04:57 +0200] rev 5710
tuned;
NEWS

1998-10-21 nipkow [Wed, 21 Oct 1998 15:57:04 +0200] rev 5709
Tutorial
NEWS

1998-10-21 wenzelm [Wed, 21 Oct 1998 14:05:49 +0200] rev 5708
dropped support for SML/NJ 109.x;
README.html etc/settings lib/scripts/run-smlnj src/Pure/ML-Systems/smlnj.ML

1998-10-21 wenzelm [Wed, 21 Oct 1998 13:31:30 +0200] rev 5707
field_injects [iffs];
src/HOL/Tools/record_package.ML