2003-12-19 nipkow [Fri, 19 Dec 2003 04:28:45 +0100] rev 14302
*** empty log message ***
src/HOL/Finite_Set.thy src/HOL/List.thy src/HOL/Nat.thy src/HOL/Set.thy

2003-12-18 paulson [Thu, 18 Dec 2003 15:06:24 +0100] rev 14301
tidied
src/HOL/Hyperreal/HyperDef.thy

2003-12-18 nipkow [Thu, 18 Dec 2003 08:20:36 +0100] rev 14300
*** empty log message ***
src/HOL/Library/List_Prefix.thy src/HOL/Library/While_Combinator.thy src/HOL/List.thy src/HOL/Map.thy

2003-12-17 paulson [Wed, 17 Dec 2003 16:23:52 +0100] rev 14299
converted Hyperreal/HyperDef to Isar script
src/HOL/Complex/NSCA.ML src/HOL/Complex/NSComplex.ML src/HOL/Hyperreal/HLog.ML src/HOL/Hyperreal/HRealAbs.ML src/HOL/Hyperreal/HRealAbs.thy src/HOL/Hyperreal/HyperDef.ML src/HOL/Hyperreal/HyperDef.thy src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/HyperOrd.thy src/HOL/Hyperreal/HyperPow.ML src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/NSA.ML src/HOL/Hyperreal/SEQ.ML src/HOL/Hyperreal/Star.ML src/HOL/Hyperreal/fuf.ML src/HOL/IsaMakefile

2003-12-16 kleing [Tue, 16 Dec 2003 23:24:17 +0100] rev 14298
fixed PG link
README.html

2003-12-16 paulson [Tue, 16 Dec 2003 15:38:09 +0100] rev 14297
converted Hyperreal/HyperOrd to new-style theory
src/HOL/Hyperreal/HyperOrd.ML src/HOL/Hyperreal/HyperOrd.thy src/HOL/Hyperreal/fuf.ML src/HOL/IsaMakefile

2003-12-15 paulson [Mon, 15 Dec 2003 17:08:41 +0100] rev 14296
updated references to the now-pornographic proofgeneral.org
doc-src/TutorialI/preface.tex doc-src/manual.bib

2003-12-15 paulson [Mon, 15 Dec 2003 16:38:25 +0100] rev 14295
more general lemmas for Ring_and_Field
doc-src/TutorialI/Types/Numbers.thy doc-src/TutorialI/Types/document/Numbers.tex doc-src/TutorialI/Types/numerics.tex src/HOL/HOL.thy src/HOL/Integ/IntArith.thy src/HOL/Real/RealArith.thy src/HOL/Ring_and_Field.thy

2003-12-13 paulson [Sat, 13 Dec 2003 09:33:52 +0100] rev 14294
absolute value theorems moved to HOL/Ring_and_Field
src/HOL/Hyperreal/HyperNat.ML src/HOL/Hyperreal/Integration.ML src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/Transcendental.ML src/HOL/Integ/Int.thy src/HOL/Real/RealArith.thy src/HOL/Ring_and_Field.thy

2003-12-12 paulson [Fri, 12 Dec 2003 15:05:18 +0100] rev 14293
moving some division theorems to Ring_and_Field
src/HOL/Hyperreal/Lim.ML src/HOL/Hyperreal/Series.ML src/HOL/Real/RealArith.thy src/HOL/Real/RealOrd.thy src/HOL/Real/real_arith.ML src/HOL/Ring_and_Field.thy