2015-09-29 wenzelm [Tue, 29 Sep 2015 13:54:04 +0200] rev 61276
clarified modules;
src/Pure/GUI/system_dialog.scala src/Pure/PIDE/batch_session.scala src/Pure/System/progress.scala src/Pure/Tools/build.scala src/Pure/Tools/build_console.scala src/Pure/Tools/build_doc.scala src/Pure/Tools/check_keywords.scala src/Pure/build-jars

2015-09-27 haftmann [Sun, 27 Sep 2015 10:11:15 +0200] rev 61275
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime
src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Library/Code_Target_Int.thy src/HOL/Library/Code_Target_Nat.thy src/HOL/NSA/StarDef.thy

2015-09-27 haftmann [Sun, 27 Sep 2015 10:11:14 +0200] rev 61274
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code
src/HOL/Code_Numeral.thy

2015-09-28 hoelzl [Mon, 28 Sep 2015 17:29:01 +0200] rev 61273
Caratheodory: cleanup and modernisation
src/HOL/Probability/Caratheodory.thy

2015-09-25 traytel [Fri, 25 Sep 2015 23:01:34 +0200] rev 61272
restructure fresh variable generation to make exports more wellformed
src/HOL/Tools/BNF/bnf_gfp.ML src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2015-09-25 traytel [Fri, 25 Sep 2015 23:01:31 +0200] rev 61271
more canonical context threading
src/HOL/Tools/BNF/bnf_def.ML src/HOL/Tools/BNF/bnf_gfp.ML src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML src/HOL/Tools/BNF/bnf_lfp.ML src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2015-09-25 wenzelm [Fri, 25 Sep 2015 23:41:24 +0200] rev 61270
merged
NEWS src/HOL/Tools/BNF/bnf_util.ML src/Pure/display.ML

2015-09-25 wenzelm [Fri, 25 Sep 2015 23:39:08 +0200] rev 61269
documentation for "Semantic subtype definitions";
misc tuning and simplification;
NEWS src/Doc/Isar_Ref/HOL_Specific.thy src/Doc/manual.bib

2015-09-25 wenzelm [Fri, 25 Sep 2015 20:37:59 +0200] rev 61268
moved remaining display.ML to more_thm.ML;
NEWS src/FOL/ex/Locale_Test/Locale_Test1.thy src/FOLP/classical.ML src/FOLP/simp.ML src/HOL/Eisbach/Eisbach_Tools.thy src/HOL/Library/Old_SMT/old_smt_normalize.ML src/HOL/Library/Old_SMT/old_smt_solver.ML src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML src/HOL/Library/old_recdef.ML src/HOL/Nominal/nominal_thmdecls.ML src/HOL/SPARK/Tools/spark_commands.ML src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/Meson/meson.ML src/HOL/Tools/Meson/meson_clausify.ML src/HOL/Tools/Metis/metis_reconstruct.ML src/HOL/Tools/Metis/metis_tactic.ML src/HOL/Tools/Predicate_Compile/code_prolog.ML src/HOL/Tools/Predicate_Compile/predicate_compile.ML src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/smt_solver.ML src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML src/HOL/Tools/choice_specification.ML src/HOL/Tools/inductive.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/lin_arith.ML src/HOL/Tools/sat.ML src/Provers/Arith/fast_lin_arith.ML src/Provers/blast.ML src/Provers/classical.ML src/Pure/Isar/attrib.ML src/Pure/Isar/bundle.ML src/Pure/Isar/calculation.ML src/Pure/Isar/code.ML src/Pure/Isar/context_rules.ML src/Pure/Isar/element.ML src/Pure/Isar/local_defs.ML src/Pure/Isar/method.ML src/Pure/Isar/obtain.ML src/Pure/Isar/proof.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Isar/runtime.ML src/Pure/Isar/token.ML src/Pure/Proof/reconstruct.ML ...

2015-09-25 wenzelm [Fri, 25 Sep 2015 20:04:25 +0200] rev 61267
less redundant output;
src/Pure/Isar/proof_display.ML src/Pure/context.ML