1997-12-28 wenzelm [Sun, 28 Dec 1997 14:55:20 +0100] rev 4484
replaced symtab.ML by table.ML;
src/Pure/IsaMakefile src/Pure/ROOT.ML src/Pure/symtab.ML

1997-12-28 wenzelm [Sun, 28 Dec 1997 14:54:38 +0100] rev 4483
renamed (is_)null to (is_)empty;
renamed DUPLICATE to DUP;
renamed extend_new to extend;
src/Pure/symtab.ML

1997-12-27 wenzelm [Sat, 27 Dec 1997 21:49:45 +0100] rev 4482
Generic tables (lacking delete operation). Implemented as 2-3 trees.
src/Pure/table.ML

1997-12-24 wenzelm [Wed, 24 Dec 1997 12:38:40 +0100] rev 4481
tuned;
README.html

1997-12-24 wenzelm [Wed, 24 Dec 1997 12:21:06 +0100] rev 4480
export range_type;
src/Pure/term.ML

1997-12-24 wenzelm [Wed, 24 Dec 1997 12:20:54 +0100] rev 4479
improved comment;
src/Pure/library.ML

1997-12-24 paulson [Wed, 24 Dec 1997 10:42:27 +0100] rev 4478
More restrictive patterns to prevent changing comments
lib/scripts/expandshort.pl

1997-12-24 paulson [Wed, 24 Dec 1997 10:02:30 +0100] rev 4477
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
src/FOL/simpdata.ML src/HOL/Auth/Event.ML src/HOL/Auth/Message.ML src/HOL/Auth/NS_Public.ML src/HOL/Auth/NS_Public_Bad.ML src/HOL/Auth/NS_Shared.ML src/HOL/Auth/OtwayRees.ML src/HOL/Auth/OtwayRees_AN.ML src/HOL/Auth/OtwayRees_Bad.ML src/HOL/Auth/Public.ML src/HOL/Auth/Recur.ML src/HOL/Auth/Shared.ML src/HOL/Auth/TLS.ML src/HOL/Auth/WooLam.ML src/HOL/Auth/Yahalom.ML src/HOL/Auth/Yahalom2.ML src/HOL/Divides.ML src/HOL/Finite.ML src/HOL/IMP/Denotation.ML src/HOL/IMP/Transition.ML src/HOL/IOA/Solve.ML src/HOL/Induct/Exp.ML src/HOL/Induct/LFilter.ML src/HOL/Induct/LList.ML src/HOL/Induct/Mutil.ML src/HOL/Integ/Integ.ML src/HOL/Option.ML src/HOL/Quot/HQUOT.ML src/HOL/Quot/NPAIR.ML src/HOL/Set.ML src/HOL/Subst/Subst.ML src/HOL/Sum.ML src/HOL/TLA/Action.ML src/HOL/TLA/Buffer/DBuffer.ML src/HOL/TLA/Inc/Inc.ML src/HOL/TLA/Memory/MIlive.ML src/HOL/TLA/Memory/MemoryImplementation.ML src/HOL/TLA/ROOT.ML src/HOL/TLA/TLA.ML src/HOL/equalities.ML src/HOL/ex/Recdef.ML src/HOL/simpdata.ML src/HOLCF/Fix.ML src/HOLCF/IOA/ABP/Correctness.ML src/HOLCF/IOA/meta_theory/Automata.ML src/HOLCF/IOA/meta_theory/CompoScheds.ML src/HOLCF/IOA/meta_theory/CompoTraces.ML src/HOLCF/IOA/meta_theory/Compositionality.ML src/HOLCF/IOA/meta_theory/RefMappings.ML src/HOLCF/IOA/meta_theory/Seq.ML ...

1997-12-23 paulson [Tue, 23 Dec 1997 11:56:09 +0100] rev 4476
Tidied using rev_iffD1
src/HOL/Auth/NS_Public_Bad.ML

1997-12-23 paulson [Tue, 23 Dec 1997 11:51:43 +0100] rev 4475
Now Blast_tac works properly
src/ZF/Ordinal.ML