2015-07-08 wenzelm [Wed, 08 Jul 2015 21:33:00 +0200] rev 60696
clarified context;
src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML src/HOL/Tools/SMT/smt_solver.ML src/HOL/Tools/cnf.ML src/HOL/Tools/reification.ML src/HOL/Tools/set_comprehension_pointfree.ML

2015-07-08 wenzelm [Wed, 08 Jul 2015 19:28:43 +0200] rev 60695
Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;
src/Doc/Implementation/Proof.thy src/HOL/Eisbach/match_method.ML src/HOL/Library/Old_SMT/old_smt_solver.ML src/HOL/Tools/Function/function_context_tree.ML src/HOL/Tools/Function/induction_schema.ML src/HOL/Tools/Function/partial_function.ML src/HOL/Tools/SMT/smt_solver.ML src/HOL/ex/Meson_Test.thy src/Pure/Isar/element.ML src/Pure/Isar/obtain.ML src/Pure/Isar/subgoal.ML src/Pure/Tools/rule_insts.ML src/Pure/goal.ML src/Pure/variable.ML src/Tools/induct_tacs.ML src/ZF/Tools/induct_tacs.ML

2015-07-08 wenzelm [Wed, 08 Jul 2015 15:37:32 +0200] rev 60694
clarified text folds: proof ... qed counts as extra block;
src/Pure/Isar/keyword.ML src/Pure/Isar/keyword.scala src/Pure/Isar/outer_syntax.scala src/Pure/Pure.thy

2015-07-08 wenzelm [Wed, 08 Jul 2015 14:30:00 +0200] rev 60693
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/keyword.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/toplevel.ML

2015-07-08 wenzelm [Wed, 08 Jul 2015 12:09:44 +0200] rev 60692
tuned;
src/Pure/Isar/keyword.scala src/Pure/Isar/outer_syntax.scala src/Pure/Isar/token.scala

2015-07-08 wenzelm [Wed, 08 Jul 2015 11:50:43 +0200] rev 60691
tuned according to a81dc82ecba3;
src/Pure/Isar/outer_syntax.ML

2015-07-08 haftmann [Wed, 08 Jul 2015 20:19:12 +0200] rev 60690
tuned facts
src/HOL/Divides.thy src/HOL/Fields.thy src/HOL/GCD.thy src/HOL/Number_Theory/Euclidean_Algorithm.thy src/HOL/Rings.thy src/HOL/ex/Sqrt.thy

2015-07-08 haftmann [Wed, 08 Jul 2015 14:01:41 +0200] rev 60689
more cautious use of [iff] declarations
src/HOL/GCD.thy

2015-07-08 haftmann [Wed, 08 Jul 2015 14:01:41 +0200] rev 60688
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
NEWS src/HOL/Equiv_Relations.thy src/HOL/GCD.thy src/HOL/Library/Poly_Deriv.thy src/HOL/Number_Theory/Cong.thy src/HOL/Number_Theory/Euclidean_Algorithm.thy src/HOL/Number_Theory/Fib.thy src/HOL/Number_Theory/Gauss.thy src/HOL/Number_Theory/Pocklington.thy src/HOL/Number_Theory/Primes.thy src/HOL/Number_Theory/Residues.thy src/HOL/Rat.thy src/HOL/Rings.thy src/HOL/Transcendental.thy

2015-07-08 haftmann [Wed, 08 Jul 2015 14:01:40 +0200] rev 60687
eliminated some duplication
src/HOL/GCD.thy src/HOL/Number_Theory/Euclidean_Algorithm.thy