2014-11-02 wenzelm [Sun, 02 Nov 2014 17:09:04 +0100] rev 58877
modernized header;
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy src/HOL/Multivariate_Analysis/Derivative.thy src/HOL/Multivariate_Analysis/Determinants.thy src/HOL/Multivariate_Analysis/Euclidean_Space.thy src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy src/HOL/Multivariate_Analysis/Fashoda.thy src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy src/HOL/Multivariate_Analysis/Integration.thy src/HOL/Multivariate_Analysis/L2_Norm.thy src/HOL/Multivariate_Analysis/Linear_Algebra.thy src/HOL/Multivariate_Analysis/Norm_Arith.thy src/HOL/Multivariate_Analysis/Operator_Norm.thy src/HOL/Multivariate_Analysis/Path_Connected.thy src/HOL/Multivariate_Analysis/PolyRoots.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Multivariate_Analysis/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 17:06:05 +0100] rev 58876
modernized header;
src/HOL/Probability/Binary_Product_Measure.thy src/HOL/Probability/Bochner_Integration.thy src/HOL/Probability/Borel_Space.thy src/HOL/Probability/Caratheodory.thy src/HOL/Probability/Convolution.thy src/HOL/Probability/Distributions.thy src/HOL/Probability/Fin_Map.thy src/HOL/Probability/Finite_Product_Measure.thy src/HOL/Probability/Independent_Family.thy src/HOL/Probability/Infinite_Product_Measure.thy src/HOL/Probability/Information.thy src/HOL/Probability/Lebesgue_Measure.thy src/HOL/Probability/Measure_Space.thy src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy src/HOL/Probability/Probability_Measure.thy src/HOL/Probability/Projective_Family.thy src/HOL/Probability/Projective_Limit.thy src/HOL/Probability/Radon_Nikodym.thy src/HOL/Probability/Regularity.thy src/HOL/Probability/Sigma_Algebra.thy src/HOL/Probability/document/root.tex src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:59:40 +0100] rev 58875
clarified legacy command;
src/Pure/Isar/isar_cmd.ML src/Pure/Isar/isar_syn.ML

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:54:06 +0100] rev 58874
modernized header;
src/HOL/Word/Bit_Representation.thy src/HOL/Word/Bits.thy src/HOL/Word/Bits_Bit.thy src/HOL/Word/Bits_Int.thy src/HOL/Word/Bool_List_Representation.thy src/HOL/Word/Examples/WordExamples.thy src/HOL/Word/Misc_Numeric.thy src/HOL/Word/Misc_Typedef.thy src/HOL/Word/Type_Length.thy src/HOL/Word/Word.thy src/HOL/Word/Word_Miscellaneous.thy src/HOL/Word/document/root.tex

2014-11-02 wenzelm [Sun, 02 Nov 2014 16:50:42 +0100] rev 58873
obsolete;
src/Doc/How_to_Prove_it/document/prelude.tex

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