2007-10-23 wenzelm [Tue, 23 Oct 2007 13:29:16 +0200] rev 25158
translations: use XCONST for input patterns (keeps original spelling of const);
src/HOLCF/Fixrec.thy

2007-10-23 paulson [Tue, 23 Oct 2007 13:10:19 +0200] rev 25157
random tidying of proofs
src/HOL/Hyperreal/Poly.thy src/HOL/List.thy src/HOL/Nat.thy src/HOL/NumberTheory/Factorization.thy src/HOL/ex/Primrec.thy

2007-10-23 wenzelm [Tue, 23 Oct 2007 12:47:21 +0200] rev 25156
empty files are back -- referenced in Makefile;
doc-src/LaTeXsugar/Sugar/document/LaTeXsugar.tex doc-src/LaTeXsugar/Sugar/document/OptionalSugar.tex

2007-10-23 haftmann [Tue, 23 Oct 2007 11:48:12 +0200] rev 25155
dropped code redundancy
src/HOL/Tools/function_package/size.ML

2007-10-23 haftmann [Tue, 23 Oct 2007 11:48:11 +0200] rev 25154
tuned
src/HOL/Tools/datatype_prop.ML

2007-10-23 haftmann [Tue, 23 Oct 2007 11:48:10 +0200] rev 25153
tuned proof
src/HOL/Hyperreal/Transcendental.thy

2007-10-23 haftmann [Tue, 23 Oct 2007 11:48:08 +0200] rev 25152
partially localized
src/HOL/Ring_and_Field.thy

2007-10-23 haftmann [Tue, 23 Oct 2007 10:53:15 +0200] rev 25151
continued
doc-src/IsarImplementation/Thy/ML.thy doc-src/IsarImplementation/Thy/document/ML.tex doc-src/IsarImplementation/Thy/document/isabelle.sty

2007-10-22 wenzelm [Mon, 22 Oct 2007 21:32:12 +0200] rev 25150
tuned;
src/Pure/Isar/theory_target.ML

2007-10-22 wenzelm [Mon, 22 Oct 2007 21:32:09 +0200] rev 25149
fixed proof: no one_is_Suc_zero;
src/HOL/Word/WordDefinition.thy