2011-09-07 blanchet [Wed, 07 Sep 2011 09:10:41 +0200] rev 44771
make mangling sound w.r.t. type arguments
src/HOL/Tools/ATP/atp_translate.ML

2011-09-07 blanchet [Wed, 07 Sep 2011 09:10:41 +0200] rev 44770
make "filter_type_args" more robust if the actual arity is higher than the declared one
src/HOL/Tools/ATP/atp_translate.ML

2011-09-07 blanchet [Wed, 07 Sep 2011 09:10:41 +0200] rev 44769
updated Sledgehammer documentation
doc-src/Sledgehammer/sledgehammer.tex

2011-09-07 blanchet [Wed, 07 Sep 2011 09:10:41 +0200] rev 44768
rationalize uniform encodings
src/HOL/Metis_Examples/Proxies.thy src/HOL/Metis_Examples/Type_Encodings.thy src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/ATP/atp_systems.ML src/HOL/Tools/ATP/atp_translate.ML src/HOL/Tools/Metis/metis_tactic.ML src/HOL/Tools/Metis/metis_translate.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

2011-09-06 huffman [Tue, 06 Sep 2011 22:41:35 -0700] rev 44767
merged

2011-09-06 huffman [Tue, 06 Sep 2011 19:03:41 -0700] rev 44766
avoid using legacy theorem names
src/HOL/Divides.thy src/HOL/GCD.thy src/HOL/Import/HOLLightInt.thy src/HOL/Library/Float.thy src/HOL/Nat_Numeral.thy src/HOL/Old_Number_Theory/Chinese.thy src/HOL/Old_Number_Theory/Euler.thy src/HOL/Old_Number_Theory/EulerFermat.thy src/HOL/Old_Number_Theory/EvenOdd.thy src/HOL/Old_Number_Theory/Finite2.thy src/HOL/Old_Number_Theory/Gauss.thy src/HOL/Old_Number_Theory/Int2.thy src/HOL/Old_Number_Theory/IntPrimes.thy src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy src/HOL/Old_Number_Theory/WilsonBij.thy src/HOL/Old_Number_Theory/WilsonRuss.thy src/HOL/Presburger.thy src/HOL/RealDef.thy

2011-09-06 huffman [Tue, 06 Sep 2011 16:30:39 -0700] rev 44765
merged

2011-09-06 huffman [Tue, 06 Sep 2011 14:53:51 -0700] rev 44764
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
src/HOL/Complex.thy src/HOL/NSA/NSComplex.thy

2011-09-07 Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 07 Sep 2011 07:59:45 +0900] rev 44763
HOL/Import: Update HOL4 generated files to current Isabelle.
src/HOL/Import/HOL/HOL4Base.thy src/HOL/Import/HOL/HOL4Prob.thy src/HOL/Import/HOL/HOL4Real.thy src/HOL/Import/HOL/HOL4Vec.thy src/HOL/Import/HOL/HOL4Word32.thy src/HOL/Import/HOL/arithmetic.imp src/HOL/Import/HOL/bits.imp src/HOL/Import/HOL/bool.imp src/HOL/Import/HOL/combin.imp src/HOL/Import/HOL/divides.imp src/HOL/Import/HOL/lim.imp src/HOL/Import/HOL/list.imp src/HOL/Import/HOL/num.imp src/HOL/Import/HOL/option.imp src/HOL/Import/HOL/pair.imp src/HOL/Import/HOL/poly.imp src/HOL/Import/HOL/prim_rec.imp src/HOL/Import/HOL/prob_extra.imp src/HOL/Import/HOL/real.imp src/HOL/Import/HOL/realax.imp src/HOL/Import/HOL/rich_list.imp src/HOL/Import/HOL/seq.imp src/HOL/Import/HOL/sum.imp src/HOL/Import/HOL/word32.imp

2011-09-07 wenzelm [Wed, 07 Sep 2011 00:08:09 +0200] rev 44762
tuned proofs;
src/HOL/Statespace/StateFun.thy src/HOL/Word/Examples/WordExamples.thy src/HOL/Word/Word.thy