2015-12-17 wenzelm [Thu, 17 Dec 2015 17:32:01 +0100] rev 61862
support pretty break indent, like underlying ML systems;
src/Pure/General/pretty.ML src/Pure/General/pretty.scala src/Pure/ML-Systems/ml_pretty.ML src/Pure/ML-Systems/polyml.ML src/Pure/ML-Systems/smlnj.ML src/Pure/PIDE/markup.ML src/Pure/PIDE/markup.scala

2015-12-19 blanchet [Sat, 19 Dec 2015 20:02:51 +0100] rev 61861
register record functions as 'Spec_Rules'
src/HOL/Tools/record.ML

2015-12-19 blanchet [Sat, 19 Dec 2015 20:02:51 +0100] rev 61860
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
src/HOL/TPTP/atp_problem_import.ML src/HOL/TPTP/atp_theory_export.ML src/HOL/Tools/ATP/atp_problem.ML src/HOL/Tools/ATP/atp_problem_generate.ML src/HOL/Tools/Metis/metis_generate.ML src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

2015-12-19 blanchet [Sat, 19 Dec 2015 20:02:51 +0100] rev 61859
removed subsumed dependency
src/HOL/Hilbert_Choice.thy

2015-12-19 blanchet [Sat, 19 Dec 2015 20:02:51 +0100] rev 61858
removed dead code
src/HOL/Tools/Nitpick/nitpick_hol.ML

2015-12-18 Andreas Lochbihler [Fri, 18 Dec 2015 14:23:11 +0100] rev 61857
add serialisation for abs on integer to target language operation
src/HOL/Code_Numeral.thy

2015-12-18 Andreas Lochbihler [Fri, 18 Dec 2015 11:14:28 +0100] rev 61856
add gcd instance for integer and serialisation to target language operations
src/HOL/Codegenerator_Test/Code_Test_GHC.thy src/HOL/Codegenerator_Test/Code_Test_OCaml.thy src/HOL/Codegenerator_Test/Code_Test_Scala.thy src/HOL/GCD.thy src/HOL/Library/Code_Target_Int.thy

2015-12-16 wenzelm [Wed, 16 Dec 2015 17:30:30 +0100] rev 61855
merged

2015-12-16 wenzelm [Wed, 16 Dec 2015 17:28:49 +0100] rev 61854
tuned whitespace;
src/Doc/Implementation/Eq.thy src/Doc/Implementation/Integration.thy src/Doc/Implementation/Isar.thy src/Doc/Implementation/Local_Theory.thy src/Doc/Implementation/Logic.thy src/Doc/Implementation/ML.thy src/Doc/Implementation/Prelim.thy src/Doc/Implementation/Proof.thy src/Doc/Implementation/Syntax.thy src/Doc/Implementation/Tactic.thy

2015-12-16 wenzelm [Wed, 16 Dec 2015 16:31:36 +0100] rev 61853
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
src/Doc/Eisbach/Manual.thy src/Doc/Implementation/Isar.thy src/Doc/Isar_Ref/Spec.thy src/HOL/Eisbach/Eisbach.thy src/HOL/Eisbach/Eisbach_Tools.thy src/HOL/Eisbach/eisbach_rule_insts.ML src/HOL/Eisbach/method_closure.ML src/HOL/TLA/Action.thy src/HOL/TLA/Intensional.thy src/HOL/TLA/TLA.thy src/HOL/Tools/Quotient/quotient_tacs.ML src/HOL/Tools/Transfer/transfer.ML src/HOL/Tools/inductive_set.ML src/HOL/Tools/legacy_transfer.ML src/HOL/Tools/split_rule.ML src/HOL/UNITY/Comp/Alloc.thy src/Provers/classical.ML src/Pure/Isar/calculation.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/rule_cases.ML src/Pure/Pure.thy src/Pure/Tools/rule_insts.ML src/Pure/more_thm.ML src/Pure/simplifier.ML src/Tools/case_product.ML src/Tools/induct.ML