1997-11-03 wenzelm [Mon, 03 Nov 1997 12:12:10 +0100] rev 4088
added thy_data;
misc fixes;
src/HOL/ROOT.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:11:34 +0100] rev 4087
use "hologic.ML"; use "cladata.ML"; use "simpdata.ML"; moved to ROOT.ML;
src/HOL/HOL.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:09:37 +0100] rev 4086
adapted to new implicit simpset;
src/HOL/simpdata.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:09:20 +0100] rev 4085
adapted to new implicit claset;
src/HOL/cladata.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:07:13 +0100] rev 4084
fixed thy dependencies;
src/HOL/indrule.thy src/HOL/intr_elim.thy

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:05:42 +0100] rev 4083
aded thy_data;
src/HOL/HOL.thy

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:04:38 +0100] rev 4082
HOL theory data.
src/HOL/thy_data.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 12:03:13 +0100] rev 4081
added thy_data.ML;
src/HOL/IsaMakefile

1997-11-03 wenzelm [Mon, 03 Nov 1997 11:56:53 +0100] rev 4080
new implicit simpset mechanism based on Sign.sg anytype data;
src/Provers/simplifier.ML

1997-11-03 wenzelm [Mon, 03 Nov 1997 11:56:36 +0100] rev 4079
new implicit claset mechanism based on Sign.sg anytype data;
tuned warnings;
src/Provers/classical.ML