2004-02-19 paulson [Thu, 19 Feb 2004 18:24:08 +0100] rev 14401
removal of the legacy ML structure List
NEWS src/HOL/Lex/MaxChop.ML src/HOL/Lex/RegExp2NA.ML src/HOL/Lex/RegExp2NAe.ML src/HOL/Lex/RegSet_of_nat_DA.ML src/HOL/List.ML src/HOL/MiniML/Type.ML src/HOLCF/IOA/ABP/Correctness.ML src/HOLCF/IOA/ABP/Lemmas.ML src/HOLCF/IOA/ABP/Lemmas.thy

2004-02-19 paulson [Thu, 19 Feb 2004 17:57:54 +0100] rev 14400
new numerics section using type classes
doc-src/TutorialI/Types/Numbers.thy doc-src/TutorialI/Types/document/Numbers.tex doc-src/TutorialI/Types/numerics.tex doc-src/TutorialI/Types/types.tex doc-src/TutorialI/tutorial.sty doc-src/TutorialI/tutorial.tex

2004-02-19 ballarin [Thu, 19 Feb 2004 16:44:21 +0100] rev 14399
New lemmas about inversion of restricted functions.
HOL-Algebra: new locale "ring" for non-commutative rings.
NEWS src/HOL/Algebra/CRing.thy src/HOL/Algebra/UnivPoly.thy src/HOL/Algebra/ringsimp.ML src/HOL/Hilbert_Choice.thy

2004-02-19 ballarin [Thu, 19 Feb 2004 15:57:34 +0100] rev 14398
Efficient, graph-based reasoner for linear and partial orders.
+ Setup as solver in the HOL simplifier.
NEWS src/HOL/Bali/DefiniteAssignmentCorrect.thy src/HOL/HOL.thy src/HOL/HoareParallel/Gar_Coll.thy src/HOL/HoareParallel/OG_Hoare.thy src/HOL/Integ/IntDef.thy src/HOL/IsaMakefile src/HOL/ROOT.ML src/HOL/Real/RealDef.thy src/HOL/Ring_and_Field.thy src/HOL/Set.thy src/HOL/SetInterval.thy src/HOL/Transitive_Closure.thy src/HOL/Wellfounded_Recursion.ML src/HOL/ex/BinEx.thy src/Provers/linorder.ML src/Provers/order.ML

2004-02-19 paulson [Thu, 19 Feb 2004 10:41:32 +0100] rev 14397
moved list_all2I to List.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy

2004-02-19 paulson [Thu, 19 Feb 2004 10:41:01 +0100] rev 14396
removed a reference to the ML structure List.thy
src/HOL/TLA/Buffer/Buffer.ML

2004-02-19 paulson [Thu, 19 Feb 2004 10:40:28 +0100] rev 14395
new theorem
src/HOL/List.thy

2004-02-19 paulson [Thu, 19 Feb 2004 10:37:15 +0100] rev 14394
comments!!
src/Pure/drule.ML

2004-02-18 paulson [Wed, 18 Feb 2004 16:01:37 +0100] rev 14393
new Union syntax
doc-src/TutorialI/Sets/sets.tex

2004-02-18 paulson [Wed, 18 Feb 2004 10:40:29 +0100] rev 14392
removed obsolete theorem
src/HOL/Real/RealPow.thy