2015-07-27 haftmann [Mon, 27 Jul 2015 22:44:02 +0200] rev 60804
formal class for factorial (semi)rings
CONTRIBUTORS src/HOL/Library/Multiset.thy src/HOL/Number_Theory/Factorial_Ring.thy src/HOL/Number_Theory/Primes.thy src/HOL/ROOT

2015-07-27 wenzelm [Mon, 27 Jul 2015 22:08:46 +0200] rev 60803
merged

2015-07-27 wenzelm [Mon, 27 Jul 2015 17:56:08 +0200] rev 60802
NEWS;
NEWS

2015-07-27 wenzelm [Mon, 27 Jul 2015 17:44:55 +0200] rev 60801
tuned signature;
src/HOL/Decision_Procs/Dense_Linear_Order.thy src/HOL/Decision_Procs/commutative_ring_tac.ML src/HOL/Decision_Procs/ferrante_rackoff.ML src/HOL/Decision_Procs/langford.ML src/HOL/HOLCF/Cfun.thy src/HOL/HOLCF/Tools/Domain/domain_constructors.ML src/HOL/HOLCF/Tools/cont_proc.ML src/HOL/HOLCF/Tools/fixrec.ML src/HOL/Import/import_rule.ML src/HOL/Library/Code_Abstract_Nat.thy src/HOL/Library/Countable.thy src/HOL/Library/Sum_of_Squares/sum_of_squares.ML src/HOL/Library/positivstellensatz.ML src/HOL/Multivariate_Analysis/normarith.ML src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_inductive.ML src/HOL/Nominal/nominal_inductive2.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/Probability/measurable.ML src/HOL/String.thy src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML src/HOL/Tools/BNF/bnf_fp_util.ML src/HOL/Tools/BNF/bnf_gfp.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML src/HOL/Tools/BNF/bnf_gfp_tactics.ML src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/BNF/bnf_lfp_tactics.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML src/HOL/Tools/Function/function_context_tree.ML src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Function/induction_schema.ML src/HOL/Tools/Function/scnp_reconstruct.ML src/HOL/Tools/Lifting/lifting_term.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Metis/metis_tactic.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/Tools/Qelim/cooper.ML src/HOL/Tools/Qelim/qelim.ML src/HOL/Tools/Quickcheck/narrowing_generators.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/Transfer/transfer.ML src/HOL/Tools/Transfer/transfer_bnf.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/cnf.ML src/HOL/Tools/code_evaluation.ML src/HOL/Tools/groebner.ML src/HOL/Tools/inductive_set.ML ...

2015-07-27 paulson <lp15@cam.ac.uk> [Mon, 27 Jul 2015 16:52:57 +0100] rev 60800
New material for Cauchy's integral theorem
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Real_Vector_Spaces.thy

2015-07-27 wenzelm [Mon, 27 Jul 2015 16:35:12 +0200] rev 60799
tuned signature for print_nested_cases;
src/Pure/Isar/proof_context.ML

2015-07-27 wenzelm [Mon, 27 Jul 2015 15:13:05 +0200] rev 60798
more explicit checks -- improved errors;
src/Pure/drule.ML

2015-07-27 wenzelm [Mon, 27 Jul 2015 14:56:06 +0200] rev 60797
eliminated cterm_instantiate;
src/Pure/drule.ML

2015-07-27 wenzelm [Mon, 27 Jul 2015 14:55:26 +0200] rev 60796
updated to infer_instantiate;
clarified context;
src/HOL/Tools/record.ML

2015-07-27 wenzelm [Mon, 27 Jul 2015 11:30:10 +0200] rev 60795
tuned signature;
src/HOL/Tools/Metis/metis_reconstruct.ML src/Pure/drule.ML