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

2004-02-17 berghofe [Tue, 17 Feb 2004 17:41:30 +0100] rev 14391
Moved application of flexflex_unique from standard' to standard.
src/Pure/drule.ML

2004-02-17 paulson [Tue, 17 Feb 2004 10:41:59 +0100] rev 14390
further tweaks to the numeric theories
src/HOL/Hyperreal/IntFloor.ML src/HOL/Integ/IntArith.thy src/HOL/Integ/NatBin.thy src/HOL/Integ/int_arith1.ML src/HOL/Integ/int_factor_simprocs.ML src/HOL/Integ/nat_simprocs.ML src/HOL/Real/rat_arith.ML src/HOL/Real/real_arith.ML