2014-11-02 wenzelm [Sun, 02 Nov 2014 16:47:45 +0100] rev 58872
added update_header tool;
NEWS lib/Tools/update_header src/Pure/Tools/update_header.scala src/Pure/build-jars

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:39:54 +0100] rev 58871
modernized header;
src/ZF/AC.thy src/ZF/Arith.thy src/ZF/ArithSimp.thy src/ZF/Bin.thy src/ZF/Bool.thy src/ZF/Cardinal.thy src/ZF/CardinalArith.thy src/ZF/Cardinal_AC.thy src/ZF/Constructible/AC_in_L.thy src/ZF/Constructible/DPow_absolute.thy src/ZF/Constructible/Datatype_absolute.thy src/ZF/Constructible/Formula.thy src/ZF/Constructible/L_axioms.thy src/ZF/Constructible/MetaExists.thy src/ZF/Constructible/Normal.thy src/ZF/Constructible/Rank.thy src/ZF/Constructible/Rank_Separation.thy src/ZF/Constructible/Rec_Separation.thy src/ZF/Constructible/Reflection.thy src/ZF/Constructible/Relative.thy src/ZF/Constructible/Satisfies_absolute.thy src/ZF/Constructible/Separation.thy src/ZF/Constructible/WF_absolute.thy src/ZF/Constructible/WFrec.thy src/ZF/Constructible/Wellorderings.thy src/ZF/Datatype_ZF.thy src/ZF/Epsilon.thy src/ZF/EquivClass.thy src/ZF/Finite.thy src/ZF/Fixedpt.thy src/ZF/IMP/Com.thy src/ZF/IMP/Denotation.thy src/ZF/IMP/Equiv.thy src/ZF/Induct/Acc.thy src/ZF/Induct/Binary_Trees.thy src/ZF/Induct/Brouwer.thy src/ZF/Induct/Comb.thy src/ZF/Induct/Datatypes.thy src/ZF/Induct/ListN.thy src/ZF/Induct/Mutil.thy src/ZF/Induct/Ntree.thy src/ZF/Induct/Primrec.thy src/ZF/Induct/PropLog.thy src/ZF/Induct/Rmap.thy src/ZF/Induct/Term.thy src/ZF/Induct/Tree_Forest.thy src/ZF/Inductive_ZF.thy src/ZF/InfDatatype.thy src/ZF/IntDiv_ZF.thy src/ZF/Int_ZF.thy ...

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:09:35 +0100] rev 58870
more flexibile \setisabellecontext, independently of header;
lib/texinputs/draft.tex lib/texinputs/isabelle.sty src/Pure/Thy/latex.ML src/Pure/Thy/present.ML

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:05:43 +0100] rev 58869
prefer explicit heading command;
src/Doc/Tutorial/Documents/Documents.thy

2014-11-02 wenzelm [Sun, 02 Nov 2014 15:27:37 +0100] rev 58868
uniform heading commands work in any context, even in theory header;
discontinued obsolete 'sect', 'subsect', 'subsubsect';
marked obsolete 'header' as legacy;
NEWS lib/texinputs/isabelle.sty src/Doc/Isar_Ref/Document_Preparation.thy src/Doc/Tutorial/Documents/Documents.thy src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML src/Pure/Isar/keyword.ML src/Pure/Isar/keyword.scala src/Pure/Isar/outer_syntax.scala src/Pure/Pure.thy src/Pure/System/options.scala src/Pure/Thy/thy_header.ML src/Pure/Thy/thy_header.scala

2014-11-02 wenzelm [Sun, 02 Nov 2014 13:26:20 +0100] rev 58867
eliminated dead code;
src/HOL/Algebra/document/root.tex src/HOL/HOLCF/Tutorial/document/root.tex

2014-11-01 wenzelm [Sat, 01 Nov 2014 20:19:07 +0100] rev 58866
clarified syntax -- avoid overlap with command category;
src/Pure/ML/ml_thms.ML src/Pure/Thy/thy_output.ML

2014-11-01 wenzelm [Sat, 01 Nov 2014 19:47:48 +0100] rev 58865
tuned signature (see ab2483fad861);
src/Pure/Isar/attrib.ML src/Pure/Isar/token.ML

2014-11-01 wenzelm [Sat, 01 Nov 2014 19:33:51 +0100] rev 58864
recover via scanner;
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML src/Pure/General/scan.ML src/Pure/General/source.ML src/Pure/General/symbol.ML src/Pure/General/symbol_pos.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/token.ML src/Pure/ML/ml_lex.ML src/Pure/ML/ml_parse.ML src/Pure/Thy/thy_header.ML src/Pure/Thy/thy_output.ML src/Pure/Thy/thy_syntax.ML

2014-11-01 wenzelm [Sat, 01 Nov 2014 18:46:48 +0100] rev 58863
simplified -- scanning is never interactive;
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML src/Pure/General/source.ML src/Pure/Isar/outer_syntax.ML src/Pure/Isar/token.ML src/Pure/ML/ml_lex.ML src/Pure/Thy/thy_header.ML