2002-02-14 nipkow [Thu, 14 Feb 2002 12:06:07 +0100] rev 12888
nodups -> distinct
src/HOL/MicroJava/J/Conform.thy src/HOL/MicroJava/J/JBasis.thy src/HOL/MicroJava/J/JTypeSafe.thy src/HOL/MicroJava/J/WellType.thy

2002-02-14 nipkow [Thu, 14 Feb 2002 11:50:52 +0100] rev 12887
nodups -> distinct
src/HOL/List.ML src/HOL/List.thy

2002-02-13 paulson [Wed, 13 Feb 2002 10:48:29 +0100] rev 12886
deleted some redundant 'addS*Es [equalityC*E]'s
src/HOL/Fun.ML src/HOL/IOA/IOA.ML src/HOL/Real/PReal.ML src/HOL/equalities.ML

2002-02-13 paulson [Wed, 13 Feb 2002 10:45:08 +0100] rev 12885
new function lemmas
src/ZF/func.ML

2002-02-13 paulson [Wed, 13 Feb 2002 10:44:39 +0100] rev 12884
tidied. no more special simpset (super_ss)
src/ZF/WF.ML

2002-02-13 paulson [Wed, 13 Feb 2002 10:44:07 +0100] rev 12883
new lemmas for closure under Union
src/ZF/Univ.ML

2002-02-12 wenzelm [Tue, 12 Feb 2002 20:35:35 +0100] rev 12882
eliminated Pure/Isar/comment.ML;
src/Pure/Isar/ROOT.ML

2002-02-12 wenzelm [Tue, 12 Feb 2002 20:34:02 +0100] rev 12881
ANTIQUOTE_FAIL;
src/Pure/Isar/antiquote.ML src/Pure/Isar/isar_output.ML src/Pure/Isar/toplevel.ML

2002-02-12 wenzelm [Tue, 12 Feb 2002 20:33:37 +0100] rev 12880
eliminated Isar/comment.ML;
src/Pure/IsaMakefile src/Pure/Isar/comment.ML

2002-02-12 wenzelm [Tue, 12 Feb 2002 20:33:03 +0100] rev 12879
tuned;
doc-src/IsarRef/generic.tex doc-src/IsarRef/intro.tex doc-src/IsarRef/isar-ref.tex doc-src/IsarRef/logics.tex doc-src/IsarRef/pure.tex doc-src/IsarRef/syntax.tex