2011-09-07 huffman [Wed, 07 Sep 2011 09:02:58 -0700] rev 44821
avoid using legacy theorem names
src/HOL/Algebra/IntRing.thy src/HOL/Algebra/UnivPoly.thy src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy src/HOL/Code_Numeral.thy src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Cooper.thy src/HOL/GCD.thy src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Number_Theory/Primes.thy src/HOL/Number_Theory/UniqueFactorization.thy src/HOL/Old_Number_Theory/Fib.thy src/HOL/Old_Number_Theory/Legacy_GCD.thy src/HOL/Old_Number_Theory/WilsonRuss.thy src/HOL/Word/Misc_Numeric.thy src/HOL/Word/Word.thy

2011-09-08 wenzelm [Thu, 08 Sep 2011 00:23:23 +0200] rev 44820
merged
CONTRIBUTORS NEWS

2011-09-07 haftmann [Wed, 07 Sep 2011 23:55:40 +0200] rev 44819
theory of saturated naturals contributed by Peter Gammie
src/HOL/Library/Saturated.thy

2011-09-07 haftmann [Wed, 07 Sep 2011 23:38:52 +0200] rev 44818
theory of saturated naturals contributed by Peter Gammie
CONTRIBUTORS NEWS src/HOL/IsaMakefile src/HOL/Library/Library.thy

2011-09-07 haftmann [Wed, 07 Sep 2011 23:07:16 +0200] rev 44817
lemmas about +, *, min, max on nat
src/HOL/Nat.thy

2011-09-07 blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44816
update Sledgehammer docs
doc-src/Sledgehammer/sledgehammer.tex

2011-09-07 blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44815
added new tagged encodings to Metis tests
src/HOL/Metis_Examples/Type_Encodings.thy

2011-09-07 blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44814
also implemented ghost version of the tagged encodings
src/HOL/Tools/ATP/atp_translate.ML

2011-09-07 blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44813
added new guards encoding to test
src/HOL/Metis_Examples/Type_Encodings.thy

2011-09-07 blanchet [Wed, 07 Sep 2011 21:31:21 +0200] rev 44812
smarter explicit apply business
src/HOL/Tools/ATP/atp_translate.ML