2009-04-29 huffman [Wed, 29 Apr 2009 17:15:01 -0700] rev 31024
reimplement reorientation simproc using theory data
src/HOL/HOL.thy src/HOL/Int.thy src/HOL/Nat.thy src/HOL/Tools/int_arith.ML src/HOLCF/Pcpo.thy

2009-04-29 huffman [Wed, 29 Apr 2009 13:36:29 -0700] rev 31023
use opaque ascription for all HOLCF code
src/HOLCF/Tools/adm_tac.ML src/HOLCF/Tools/cont_consts.ML src/HOLCF/Tools/cont_proc.ML src/HOLCF/Tools/domain/domain_axioms.ML src/HOLCF/Tools/domain/domain_extender.ML src/HOLCF/Tools/domain/domain_library.ML src/HOLCF/Tools/domain/domain_syntax.ML src/HOLCF/Tools/domain/domain_theorems.ML src/HOLCF/Tools/fixrec_package.ML src/HOLCF/Tools/pcpodef_package.ML

2009-04-29 nipkow [Wed, 29 Apr 2009 21:10:46 +0200] rev 31022
added listsum lemmas
src/HOL/List.thy

2009-04-29 haftmann [Wed, 29 Apr 2009 14:20:26 +0200] rev 31021
farewell to class recpower
src/HOL/Algebra/poly/UnivPoly2.thy src/HOL/Complex.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy src/HOL/Int.thy src/HOL/Library/Binomial.thy src/HOL/Library/Commutative_Ring.thy src/HOL/Library/Euclidean_Space.thy src/HOL/Library/Float.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/FrechetDeriv.thy src/HOL/Library/Fundamental_Theorem_Algebra.thy src/HOL/Library/Numeral_Type.thy src/HOL/Library/Pocklington.thy src/HOL/Library/Polynomial.thy src/HOL/Library/Univ_Poly.thy src/HOL/Library/comm_ring.ML src/HOL/NSA/StarDef.thy src/HOL/Power.thy src/HOL/Rational.thy src/HOL/RealPow.thy src/HOL/SizeChange/Graphs.thy src/HOL/SizeChange/Kleene_Algebras.thy src/HOL/Word/WordArith.thy src/HOL/ex/Commutative_Ring_Complete.thy src/HOL/ex/Formal_Power_Series_Examples.thy src/HOL/ex/Groebner_Examples.thy src/HOL/ex/Numeral.thy src/HOL/ex/ReflectionEx.thy

2009-04-28 haftmann [Tue, 28 Apr 2009 19:15:50 +0200] rev 31020
merged

2009-04-28 haftmann [Tue, 28 Apr 2009 16:58:23 +0200] rev 31019
power constraint needed, though
src/HOL/NSA/NSComplex.thy

2009-04-28 haftmann [Tue, 28 Apr 2009 15:50:32 +0200] rev 31018
stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy
src/HOL/Word/Num_Lemmas.thy

2009-04-28 haftmann [Tue, 28 Apr 2009 15:50:30 +0200] rev 31017
stripped class recpower further
src/HOL/Deriv.thy src/HOL/Finite_Set.thy src/HOL/Groebner_Basis.thy src/HOL/Lim.thy src/HOL/NSA/HDeriv.thy src/HOL/NSA/HSEQ.thy src/HOL/NSA/HyperDef.thy src/HOL/NSA/NSA.thy src/HOL/NSA/NSComplex.thy src/HOL/Parity.thy src/HOL/Rational.thy src/HOL/RealVector.thy src/HOL/SEQ.thy src/HOL/Series.thy src/HOL/SetInterval.thy src/HOL/Transcendental.thy src/HOL/Word/WordArith.thy

2009-04-28 haftmann [Tue, 28 Apr 2009 15:50:30 +0200] rev 31016
lemma sum_nonneg_eq_zero_iff
src/HOL/OrderedGroup.thy

2009-04-28 haftmann [Tue, 28 Apr 2009 15:50:29 +0200] rev 31015
reorganization of power lemmas
src/HOL/Int.thy