2015-06-02 wenzelm [Tue, 02 Jun 2015 09:16:19 +0200] rev 60358
clarified context;
src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Metis/metis_generate.ML src/HOL/Tools/Metis/metis_tactic.ML src/Tools/IsaPlanner/isand.ML src/Tools/IsaPlanner/rw_inst.ML src/Tools/eqsubst.ML src/Tools/misc_legacy.ML

2015-06-02 wenzelm [Tue, 02 Jun 2015 09:10:05 +0200] rev 60357
tuned proof;
src/HOL/GCD.thy

2015-06-03 noschinl [Wed, 03 Jun 2015 09:32:49 +0200] rev 60356
merged

2015-06-02 noschinl [Tue, 02 Jun 2015 13:14:36 +0200] rev 60355
simps_of_case: Better error if split rule is not an equality
src/HOL/Library/simps_case_conv.ML

2015-06-02 noschinl [Tue, 02 Jun 2015 13:14:11 +0200] rev 60354
simps_of_case: allow Drule.dummy_thm as ignored split rule
src/HOL/Library/simps_case_conv.ML

2015-06-01 haftmann [Mon, 01 Jun 2015 18:59:22 +0200] rev 60353
implicit partial divison operation in integral domains
src/HOL/Divides.thy src/HOL/Fields.thy src/HOL/Groups_Big.thy src/HOL/NSA/StarDef.thy src/HOL/Nat.thy src/HOL/Rings.thy

2015-06-01 haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60352
separate class for division operator, with particular syntax added in more specific classes
NEWS src/Doc/Main/Main_Doc.thy src/HOL/Code_Numeral.thy src/HOL/Complex.thy src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy src/HOL/Divides.thy src/HOL/Enum.thy src/HOL/Fields.thy src/HOL/Library/Bit.thy src/HOL/Library/Extended_Real.thy src/HOL/Library/Fraction_Field.thy src/HOL/Library/Function_Division.thy src/HOL/Library/Nat_Bijection.thy src/HOL/Library/Old_SMT/old_smt_normalize.ML src/HOL/Library/Old_SMT/old_z3_interface.ML src/HOL/Library/Polynomial.thy src/HOL/Library/Predicate_Compile_Alternative_Defs.thy src/HOL/Mutabelle/mutabelle_extra.ML src/HOL/NSA/StarDef.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Rings.thy src/HOL/SMT_Examples/SMT_Examples.certs src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/SMT/z3_interface.ML src/HOL/Tools/SMT/z3_real.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/nat_numeral_simprocs.ML src/HOL/Tools/numeral_simprocs.ML src/HOL/Tools/semiring_normalizer.ML src/HOL/Word/Word.thy src/HOL/ex/Dedekind_Real.thy

2015-06-01 haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60351
explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
src/HOL/Tools/lin_arith.ML

2015-06-01 haftmann [Mon, 01 Jun 2015 18:59:21 +0200] rev 60350
dropped dead config option
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/try0.ML

2015-06-01 haftmann [Mon, 01 Jun 2015 18:59:20 +0200] rev 60349
tuned, including proper signature for functor argument
src/HOL/Tools/lin_arith.ML