2015-09-24 wenzelm [Thu, 24 Sep 2015 23:33:29 +0200] rev 61261
more explicit Defs.context: use proper name spaces as far as possible;
src/Doc/Implementation/Logic.thy src/HOL/Tools/typedef.ML src/Pure/Isar/generic_target.ML src/Pure/Isar/proof_context.ML src/Pure/Isar/proof_display.ML src/Pure/Isar/typedecl.ML src/Pure/ROOT.ML src/Pure/defs.ML src/Pure/global_theory.ML src/Pure/more_thm.ML src/Pure/theory.ML

2015-09-24 wenzelm [Thu, 24 Sep 2015 13:33:42 +0200] rev 61260
explicit indication of overloaded typedefs;
src/Doc/Isar_Ref/HOL_Specific.thy src/HOL/Datatype_Examples/Misc_N2M.thy src/HOL/Datatype_Examples/Stream_Processor.thy src/HOL/HOLCF/Porder.thy src/HOL/HOLCF/Tools/cpodef.ML src/HOL/IMP/Abs_State.thy src/HOL/Import/import_rule.ML src/HOL/Library/Fraction_Field.thy src/HOL/Library/Polynomial.thy src/HOL/Library/Quotient_Type.thy src/HOL/Library/RBT.thy src/HOL/Library/Saturated.thy src/HOL/Matrix_LP/Matrix.thy src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy src/HOL/Nominal/Nominal.thy src/HOL/Nominal/nominal_datatype.ML src/HOL/SPARK/Tools/spark_vcs.ML src/HOL/Tools/BNF/bnf_util.ML src/HOL/Tools/Old_Datatype/old_datatype.ML src/HOL/Tools/Quotient/quotient_type.ML src/HOL/Tools/record.ML src/HOL/Tools/typedef.ML src/HOL/Word/Word.thy src/HOL/ex/PER.thy src/Pure/Isar/parse_spec.ML src/Pure/defs.ML

2015-09-23 wenzelm [Wed, 23 Sep 2015 09:50:38 +0200] rev 61259
tuned signature;
src/HOL/Library/bnf_axiomatization.ML src/HOL/SPARK/Tools/spark_vcs.ML src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML src/HOL/Tools/BNF/bnf_fp_def_sugar.ML src/HOL/Tools/typedef.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/typedecl.ML

2015-09-23 wenzelm [Wed, 23 Sep 2015 09:36:18 +0200] rev 61258
tuned output;
src/Pure/Isar/proof_display.ML

2015-09-23 wenzelm [Wed, 23 Sep 2015 09:30:12 +0200] rev 61257
tuned output;
src/Pure/Isar/proof_display.ML

2015-09-22 wenzelm [Tue, 22 Sep 2015 22:42:48 +0200] rev 61256
tuned signature;
src/Pure/Isar/proof_display.ML src/Pure/axclass.ML src/Pure/defs.ML src/Pure/pure_thy.ML src/Pure/theory.ML

2015-09-22 wenzelm [Tue, 22 Sep 2015 22:38:22 +0200] rev 61255
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
Object_Logic.add_judgment more like Theory.specify_const;
src/Doc/Implementation/Logic.thy src/HOL/Tools/typedef.ML src/Pure/Isar/object_logic.ML src/Pure/Isar/typedecl.ML src/Pure/axclass.ML src/Pure/pure_thy.ML src/Pure/theory.ML

2015-09-22 wenzelm [Tue, 22 Sep 2015 20:29:20 +0200] rev 61254
tuned signature;
src/Pure/defs.ML

2015-09-22 wenzelm [Tue, 22 Sep 2015 20:21:53 +0200] rev 61253
tuned output;
src/Pure/Isar/proof_display.ML src/Pure/defs.ML

2015-09-22 wenzelm [Tue, 22 Sep 2015 18:56:25 +0200] rev 61252
separate command 'print_definitions';
NEWS src/Doc/Isar_Ref/Outer_Syntax.thy src/Pure/Isar/isar_syn.ML src/Pure/Isar/proof_display.ML src/Pure/Pure.thy src/Pure/display.ML