2014-11-09 wenzelm [Sun, 09 Nov 2014 17:04:14 +0100] rev 58957
proper context for match_tac etc.;
NEWS src/CCL/Wfd.thy src/Doc/Implementation/Tactic.thy src/FOL/FOL.thy src/FOL/intprover.ML src/FOL/simpdata.ML src/FOLP/FOLP.thy src/FOLP/classical.ML src/FOLP/ex/Classical.thy src/FOLP/ex/If.thy src/FOLP/ex/Intro.thy src/FOLP/ex/Propositional_Cla.thy src/FOLP/ex/Quantifiers_Cla.thy src/HOL/HOL.thy src/HOL/HOLCF/Cfun.thy src/HOL/HOLCF/IOA/meta_theory/Automata.thy src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML src/HOL/HOLCF/Tools/fixrec.ML src/HOL/Library/Old_SMT/old_z3_proof_methods.ML src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML src/HOL/NSA/transfer.ML src/HOL/Nominal/nominal_induct.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/SMT/z3_replay_methods.ML src/HOL/Tools/simpdata.ML src/Provers/blast.ML src/Provers/classical.ML src/Provers/hypsubst.ML src/Pure/Isar/class_declaration.ML src/Pure/Isar/method.ML src/Pure/simplifier.ML src/Pure/tactic.ML src/Sequents/simpdata.ML src/Tools/induct.ML src/Tools/intuitionistic.ML

2014-11-09 wenzelm [Sun, 09 Nov 2014 14:08:00 +0100] rev 58956
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
NEWS src/Doc/Implementation/Tactic.thy src/HOL/Decision_Procs/ferrack_tac.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/HOL.thy src/HOL/HOLCF/Tr.thy src/HOL/Library/simps_case_conv.ML src/HOL/List.thy src/HOL/Nominal/nominal_datatype.ML src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/Nominal/nominal_permeq.ML src/HOL/Nominal/nominal_primrec.ML src/HOL/SPARK/Tools/spark_vcs.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/Tools/Old_Datatype/old_datatype_aux.ML src/HOL/Tools/Old_Datatype/old_rep_datatype.ML src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/SMT/z3_replay_methods.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/record.ML src/HOL/ex/SVC_Oracle.thy src/HOL/ex/svc_test.thy src/Provers/blast.ML src/Provers/hypsubst.ML src/Provers/splitter.ML src/Pure/Isar/expression.ML src/Pure/Tools/rule_insts.ML src/Pure/tactic.ML src/Tools/atomize_elim.ML src/Tools/cong_tac.ML src/Tools/induct.ML

2014-11-09 nipkow [Sun, 09 Nov 2014 11:05:20 +0100] rev 58955
avoid erule and rotated in IMP
src/HOL/IMP/Abs_Int0.thy

2014-11-09 haftmann [Sun, 09 Nov 2014 10:03:18 +0100] rev 58954
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
src/HOL/Number_Theory/Primes.thy

2014-11-09 haftmann [Sun, 09 Nov 2014 10:03:17 +0100] rev 58953
self-contained simp rules for dvd on numerals
src/HOL/Divides.thy src/HOL/Matrix_LP/ComputeNumeral.thy src/HOL/Number_Theory/Euclidean_Algorithm.thy

2014-11-08 haftmann [Sat, 08 Nov 2014 16:53:26 +0100] rev 58952
equivalence rules for structures without zero divisors
src/HOL/Nat.thy src/HOL/Rings.thy

2014-11-08 wenzelm [Sat, 08 Nov 2014 22:10:16 +0100] rev 58951
removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
src/Pure/config.ML

2014-11-08 wenzelm [Sat, 08 Nov 2014 21:31:51 +0100] rev 58950
optional proof context for unify operations, for the sake of proper local options;
src/Doc/Implementation/Tactic.thy src/HOL/Nominal/nominal_fresh_fun.ML src/HOL/TLA/Intensional.thy src/HOL/Tools/Function/function_core.ML src/HOL/Tools/Function/induction_schema.ML src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/TFL/casesplit.ML src/Provers/blast.ML src/Provers/classical.ML src/Provers/hypsubst.ML src/Pure/Isar/calculation.ML src/Pure/Isar/method.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/rule_cases.ML src/Pure/Proof/extraction.ML src/Pure/Proof/reconstruct.ML src/Pure/Tools/rule_insts.ML src/Pure/drule.ML src/Pure/goal.ML src/Pure/par_tactical.ML src/Pure/pattern.ML src/Pure/raw_simplifier.ML src/Pure/subgoal.ML src/Pure/tactic.ML src/Pure/thm.ML src/Pure/unify.ML src/Tools/eqsubst.ML src/Tools/induct.ML src/Tools/misc_legacy.ML

2014-11-08 wenzelm [Sat, 08 Nov 2014 17:39:01 +0100] rev 58949
clarified name of Type.unified, to emphasize its connection to the "unify" family;
tuned low-level operation;
src/Pure/envir.ML src/Pure/type.ML

2014-11-08 wenzelm [Sat, 08 Nov 2014 16:55:41 +0100] rev 58948
proper Envir.norm_type for result of Type.raw_unifys;
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML