2015-12-28 wenzelm [Mon, 28 Dec 2015 01:26:34 +0100] rev 61944
prefer symbols for "abs";
src/HOL/Archimedean_Field.thy src/HOL/Complex.thy src/HOL/Divides.thy src/HOL/Fields.thy src/HOL/GCD.thy src/HOL/Groups.thy src/HOL/Groups_Big.thy src/HOL/Int.thy src/HOL/MacLaurin.thy src/HOL/Nitpick.thy src/HOL/NthRoot.thy src/HOL/Num.thy src/HOL/Power.thy src/HOL/Presburger.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Rings.thy src/HOL/Transcendental.thy

2015-12-27 wenzelm [Sun, 27 Dec 2015 22:07:17 +0100] rev 61943
discontinued ASCII replacement syntax <*>;
NEWS src/Doc/Main/Main_Doc.thy src/HOL/BNF_Cardinal_Arithmetic.thy src/HOL/BNF_Cardinal_Order_Relation.thy src/HOL/BNF_Greatest_Fixpoint.thy src/HOL/BNF_Wellorder_Constructions.thy src/HOL/Cardinals/Cardinal_Arithmetic.thy src/HOL/Cardinals/Cardinal_Order_Relation.thy src/HOL/Groups_Big.thy src/HOL/Induct/SList.thy src/HOL/Induct/Sexp.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Old_Datatype.thy src/HOL/MicroJava/BV/JVMType.thy src/HOL/MicroJava/DFA/Product.thy src/HOL/Nominal/Examples/Class3.thy src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy src/HOL/Product_Type.thy src/HOL/UNITY/Comp/TimerArray.thy src/HOL/UNITY/Extend.thy src/HOL/UNITY/Lift_prog.thy src/HOL/UNITY/PPROD.thy src/HOL/Wellfounded.thy

2015-12-27 wenzelm [Sun, 27 Dec 2015 21:46:36 +0100] rev 61942
prefer symbols for "floor", "ceiling";
src/HOL/Archimedean_Field.thy src/HOL/Decision_Procs/MIR.thy src/HOL/Library/Float.thy src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy src/HOL/Multivariate_Analysis/Complex_Transcendental.thy src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy src/HOL/Probability/Bochner_Integration.thy src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy src/HOL/Rat.thy src/HOL/Real.thy src/HOL/Real_Vector_Spaces.thy src/HOL/TPTP/THF_Arith.thy src/HOL/Transcendental.thy

2015-12-27 wenzelm [Sun, 27 Dec 2015 17:16:21 +0100] rev 61941
discontinued ASCII replacement syntax <->;
NEWS src/HOL/Fields.thy src/HOL/HOL.thy src/HOL/List.thy src/HOL/Meson.thy src/HOL/TLA/Memory/MemoryImplementation.thy src/HOL/UNITY/Comp.thy src/HOL/UNITY/Comp/Priority.thy src/HOL/UNITY/Extend.thy src/HOL/UNITY/Union.thy src/HOL/Word/Bit_Representation.thy src/HOL/Word/Misc_Typedef.thy src/HOL/Word/Word.thy

2015-12-27 wenzelm [Sun, 27 Dec 2015 16:40:09 +0100] rev 61940
more symbols;
src/HOL/Tools/ATP/atp_problem_generate.ML

2015-12-27 wenzelm [Sun, 27 Dec 2015 16:20:02 +0100] rev 61939
tuned document;
src/HOL/Isar_Examples/Schroeder_Bernstein.thy src/HOL/Isar_Examples/document/root.tex src/HOL/ROOT

2015-12-27 wenzelm [Sun, 27 Dec 2015 16:00:41 +0100] rev 61938
more proofs;
src/HOL/Isar_Examples/Schroeder_Bernstein.thy src/HOL/ROOT

2015-12-27 wenzelm [Sun, 27 Dec 2015 15:52:43 +0100] rev 61937
tuned;
src/HOL/ex/Set_Theory.thy

2015-12-26 wenzelm [Sat, 26 Dec 2015 19:37:06 +0100] rev 61936
more notation;
more examples;
src/HOL/Isar_Examples/Higher_Order_Logic.thy

2015-12-26 wenzelm [Sat, 26 Dec 2015 19:27:46 +0100] rev 61935
clarified sessions;
src/FOL/ROOT src/FOL/ex/First_Order_Logic.thy src/HOL/Induct/Nested_Datatype.thy src/HOL/Isar_Examples/First_Order_Logic.thy src/HOL/Isar_Examples/Higher_Order_Logic.thy src/HOL/Isar_Examples/Nested_Datatype.thy src/HOL/Isar_Examples/document/root.bib src/HOL/Isar_Examples/document/root.tex src/HOL/ROOT src/HOL/ex/Higher_Order_Logic.thy src/HOL/ex/document/root.bib