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

1998-02-27 oheimb [Fri, 27 Feb 1998 11:18:29 +0100] rev 4665
added minimal description of rep_cs
doc-src/Ref/classical.tex

1998-02-27 oheimb [Fri, 27 Feb 1998 11:18:16 +0100] rev 4664
added minimal description of rep_ss
doc-src/Ref/simplifier.tex

1998-02-27 paulson [Fri, 27 Feb 1998 11:08:20 +0100] rev 4663
"choice" moved to Set.ML
src/HOL/ex/meson.ML