1998-03-03 paulson [Tue, 03 Mar 1998 15:13:24 +0100] rev 4675
New theorem
src/HOL/arith_data.ML

1998-03-03 paulson [Tue, 03 Mar 1998 15:12:57 +0100] rev 4674
New theorems
src/HOL/Vimage.ML src/HOL/equalities.ML

1998-03-03 paulson [Tue, 03 Mar 1998 15:12:25 +0100] rev 4673
New theorems; tidied
src/HOL/Relation.ML

1998-03-03 paulson [Tue, 03 Mar 1998 15:11:26 +0100] rev 4672
New theorem diff_Suc_le_Suc_diff; tidied another proof
src/HOL/Arith.ML

1998-03-03 paulson [Tue, 03 Mar 1998 15:09:04 +0100] rev 4671
auto generated
doc-src/Ref/ref.ind

1998-02-28 nipkow [Sat, 28 Feb 1998 15:41:50 +0100] rev 4670
Modified def.
src/HOL/Lex/Auto.ML src/HOL/Lex/Auto.thy

1998-02-28 nipkow [Sat, 28 Feb 1998 15:41:17 +0100] rev 4669
Splitters via named loopers.
src/FOL/simpdata.ML src/HOL/simpdata.ML

1998-02-28 nipkow [Sat, 28 Feb 1998 15:40:50 +0100] rev 4668
Little reorganization. Loop tactics have names now.
src/Provers/simplifier.ML src/Provers/splitter.ML

1998-02-28 nipkow [Sat, 28 Feb 1998 15:40:03 +0100] rev 4667
Tried to reorganize rewriter a little. More to be done.
src/Pure/logic.ML src/Pure/pattern.ML src/Pure/thm.ML

1998-02-27 oheimb [Fri, 27 Feb 1998 11:21:28 +0100] rev 4666
added minimal description of rep_cs: corrections
doc-src/Ref/classical.tex