2015-06-25 haftmann [Thu, 25 Jun 2015 15:01:41 +0200] rev 60569
generalized to definition from literature, which covers also polynomials
src/HOL/Number_Theory/Euclidean_Algorithm.thy

2015-06-25 blanchet [Thu, 25 Jun 2015 12:41:43 +0200] rev 60568
put E before (typically remote, hence less reliable) Vampire
src/Doc/Sledgehammer/document/root.tex src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

2015-06-24 wenzelm [Wed, 24 Jun 2015 23:03:55 +0200] rev 60567
tuned proofs -- less digits;
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Decision_Procs/Rat_Pair.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Fundamental_Theorem_Algebra.thy src/HOL/Number_Theory/UniqueFactorization.thy

2015-06-24 wenzelm [Wed, 24 Jun 2015 21:31:29 +0200] rev 60566
updated to scala-2.11.7;
Admin/components/components.sha1 Admin/components/main

2015-06-24 wenzelm [Wed, 24 Jun 2015 21:26:03 +0200] rev 60565
clarified 'case' command;
NEWS src/Doc/Isar_Ref/Proof.thy src/HOL/Library/FinFun.thy src/HOL/MicroJava/J/Eval.thy src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML

2015-06-24 blanchet [Wed, 24 Jun 2015 00:30:03 +0200] rev 60564
silence 'try'
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

2015-06-23 paulson <lp15@cam.ac.uk> [Tue, 23 Jun 2015 16:56:40 +0100] rev 60563
Merge

2015-06-23 paulson <lp15@cam.ac.uk> [Tue, 23 Jun 2015 16:55:28 +0100] rev 60562
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Library/Function_Algebras.thy src/HOL/Library/Polynomial.thy src/HOL/NSA/StarDef.thy src/HOL/Nat.thy src/HOL/Parity.thy src/HOL/Rings.thy

2015-06-23 wenzelm [Tue, 23 Jun 2015 17:20:16 +0200] rev 60561
tuned proofs;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

2015-06-22 wenzelm [Mon, 22 Jun 2015 23:19:48 +0200] rev 60560
tuned proofs;
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy