2014-10-30 haftmann [Thu, 30 Oct 2014 21:02:01 +0100] rev 58834
more simp rules concerning dvd and even/odd
src/HOL/Decision_Procs/Approximation.thy src/HOL/Decision_Procs/Commutative_Ring.thy src/HOL/Decision_Procs/Rat_Pair.thy src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy src/HOL/Divides.thy src/HOL/GCD.thy src/HOL/Library/Float.thy src/HOL/Library/Nat_Bijection.thy src/HOL/Number_Theory/Gauss.thy src/HOL/Number_Theory/Pocklington.thy src/HOL/Old_Number_Theory/Legacy_GCD.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Transcendental.thy src/HOL/Word/Bit_Representation.thy

2014-10-30 paulson <lp15@cam.ac.uk> [Thu, 30 Oct 2014 16:36:44 +0000] rev 58833
choose_reduce_nat: re-ordered operands
src/HOL/Number_Theory/Binomial.thy

2014-10-30 wenzelm [Thu, 30 Oct 2014 11:24:53 +0100] rev 58832
make SML/NJ more happy;
src/HOL/Library/code_test.ML

2014-10-30 wenzelm [Thu, 30 Oct 2014 11:08:26 +0100] rev 58831
proper syntax categery "name" -- as usual and as documented;
src/HOL/Library/bnf_axiomatization.ML src/HOL/Tools/BNF/bnf_util.ML src/HOL/Tools/Metis/metis_tactic.ML src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

2014-10-30 hoelzl [Thu, 30 Oct 2014 09:15:54 +0100] rev 58830
disable coercions for NO_MATCH
src/HOL/HOL.thy

2014-10-29 wenzelm [Wed, 29 Oct 2014 19:26:05 +0100] rev 58829
merged

2014-10-29 wenzelm [Wed, 29 Oct 2014 19:13:19 +0100] rev 58828
modernized setup;
src/ZF/Inductive_ZF.thy src/ZF/Tools/ind_cases.ML src/ZF/Tools/induct_tacs.ML src/ZF/Tools/typechk.ML src/ZF/upair.thy

2014-10-29 wenzelm [Wed, 29 Oct 2014 19:23:32 +0100] rev 58827
merged
src/HOL/Library/Lubs_Glbs.thy src/HOL/Tools/Function/context_tree.ML

2014-10-29 wenzelm [Wed, 29 Oct 2014 19:01:49 +0100] rev 58826
modernized setup;
src/FOL/FOL.thy src/FOL/IFOL.thy src/HOL/BNF_Greatest_Fixpoint.thy src/HOL/Fields.thy src/HOL/Fun_Def.thy src/HOL/HOL.thy src/HOL/Orderings.thy src/HOL/Product_Type.thy src/HOL/Quickcheck_Exhaustive.thy src/HOL/Quickcheck_Narrowing.thy src/HOL/Quickcheck_Random.thy src/HOL/Semiring_Normalization.thy src/HOL/Tools/Function/fun.ML src/HOL/Tools/Function/function.ML src/HOL/Tools/Quickcheck/exhaustive_generators.ML src/HOL/Tools/Quickcheck/narrowing_generators.ML src/HOL/Tools/Quickcheck/random_generators.ML src/HOL/Tools/semiring_normalizer.ML src/Provers/blast.ML src/Provers/clasimp.ML src/Provers/classical.ML src/Provers/hypsubst.ML src/Provers/splitter.ML src/Tools/case_product.ML src/Tools/eqsubst.ML src/Tools/induct.ML src/Tools/induct_tacs.ML src/Tools/induction.ML src/Tools/subtyping.ML

2014-10-29 wenzelm [Wed, 29 Oct 2014 17:01:44 +0100] rev 58825
modernized setup;
src/HOL/Library/Old_Recdef.thy src/HOL/Library/Old_SMT.thy src/HOL/Library/Old_SMT/old_smt_real.ML src/HOL/Library/Old_SMT/old_smt_word.ML src/HOL/Library/Refute.thy src/HOL/Library/refute.ML src/HOL/NSA/StarDef.thy src/HOL/NSA/transfer.ML src/HOL/Statespace/StateSpaceLocale.thy src/HOL/Statespace/state_fun.ML src/HOL/Tools/recdef.ML