2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:38 +0100] rev 35050
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
NEWS src/HOL/Algebra/poly/UnivPoly2.thy src/HOL/Decision_Procs/mir_tac.ML src/HOL/Divides.thy src/HOL/Fields.thy src/HOL/Groebner_Basis.thy src/HOL/Groups.thy src/HOL/Import/HOL/arithmetic.imp src/HOL/Import/HOL/divides.imp src/HOL/Import/HOL/prob_extra.imp src/HOL/Import/HOL/real.imp src/HOL/Import/HOL/realax.imp src/HOL/Int.thy src/HOL/IsaMakefile src/HOL/Library/Poly_Deriv.thy src/HOL/Metis_Examples/BigO.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/NSComplex.thy src/HOL/NSA/StarDef.thy src/HOL/OrderedGroup.thy src/HOL/PReal.thy src/HOL/Presburger.thy src/HOL/Probability/Borel.thy src/HOL/RealDef.thy src/HOL/Ring_and_Field.thy src/HOL/Rings.thy src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Tools/numeral_simprocs.ML

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:32 +0100] rev 35049
tuned spelling
src/HOL/Word/Word.thy

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:30 +0100] rev 35048
tuned proofs
src/HOL/Old_Number_Theory/WilsonBij.thy src/HOL/Old_Number_Theory/WilsonRuss.thy src/HOL/Word/BinGeneral.thy

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:27 +0100] rev 35047
hide fact Nat.add_0_right; make add_0_right from Groups priority
src/HOL/Nat.thy src/HOL/Nat_Numeral.thy src/HOL/Tools/Function/size.ML src/HOL/Tools/nat_arith.ML

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:24 +0100] rev 35046
tuned header
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:22 +0100] rev 35045
using code antiquotation
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

2010-02-08 haftmann [Mon, 08 Feb 2010 17:12:18 +0100] rev 35044
tuned header
src/HOL/Decision_Procs/Decision_Procs.thy

2010-02-08 haftmann [Mon, 08 Feb 2010 14:22:22 +0100] rev 35043
dropped accidental duplication of "lin" prefix from cs. 108662d50512
src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Multivariate_Analysis/Euclidean_Space.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/StarDef.thy src/HOL/Nat_Numeral.thy src/HOL/Parity.thy src/HOL/Ring_and_Field.thy src/HOL/Tools/numeral_simprocs.ML

2010-02-08 haftmann [Mon, 08 Feb 2010 14:22:22 +0100] rev 35042
NEWS: ax_simps
NEWS

2010-02-08 haftmann [Mon, 08 Feb 2010 14:12:50 +0100] rev 35041
avoid upto in generated code (is infix operator in library.ML)
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy src/HOL/Imperative_HOL/ex/Linked_Lists.thy