2016-12-18 wenzelm [Sun, 18 Dec 2016 12:32:20 +0100] rev 64594
more permissive syntax;
more PIDE markup;
src/Pure/ML/ml_antiquotations.ML

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:14 +0100] rev 64593
reoriented congruence rules in non-explosive direction
NEWS src/HOL/Analysis/Complex_Transcendental.thy src/HOL/Decision_Procs/cooper_tac.ML src/HOL/Decision_Procs/mir_tac.ML src/HOL/Divides.thy src/HOL/Groebner_Basis.thy src/HOL/IMP/Abs_Int1_parity.thy src/HOL/Library/Numeral_Type.thy src/HOL/Library/Omega_Words_Fun.thy src/HOL/Number_Theory/Cong.thy src/HOL/Number_Theory/Pocklington.thy src/HOL/Number_Theory/Quadratic_Reciprocity.thy src/HOL/Number_Theory/Residues.thy src/HOL/SPARK/Examples/RIPEMD-160/Round.thy src/HOL/SPARK/Manual/Proc1.thy src/HOL/SPARK/Manual/Proc2.thy src/HOL/Tools/Qelim/cooper.ML src/HOL/Word/Bit_Representation.thy src/HOL/Word/Bits_Int.thy src/HOL/Word/Misc_Numeric.thy src/HOL/Word/Word.thy src/HOL/Word/Word_Miscellaneous.thy src/HOL/ex/Word_Type.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:14 +0100] rev 64592
more fine-grained type class hierarchy for div and mod
src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Enum.thy src/HOL/Library/Formal_Power_Series.thy src/HOL/Library/Normalized_Fraction.thy src/HOL/Library/Polynomial.thy src/HOL/Number_Theory/Euclidean_Algorithm.thy src/HOL/Rings.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64591
restructured matter on polynomials and normalized fractions
src/HOL/Fields.thy src/HOL/Fun_Def.thy src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy src/HOL/Library/Field_as_Ring.thy src/HOL/Library/Multiset.thy src/HOL/Library/Normalized_Fraction.thy src/HOL/Library/Polynomial.thy src/HOL/Library/Polynomial_Factorial.thy src/HOL/ROOT src/HOL/Rings.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64590
streamlined computation rules for primality of numerals: no need to go via explicit conversion to nat
src/HOL/Number_Theory/Primes.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64589
tuned fact references
src/HOL/Tools/Qelim/cooper.ML

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64588
clarified library contents
src/HOL/Library/Library.thy src/HOL/ROOT

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:13 +0100] rev 64587
standardized notation
src/HOL/Algebra/Coset.thy src/HOL/Algebra/Divisibility.thy src/HOL/Library/DAList_Multiset.thy src/HOL/Library/Multiset.thy src/HOL/Library/Multiset_Order.thy src/HOL/Library/Permutation.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64586
redundant
src/HOL/Library/Multiset.thy

2016-12-17 haftmann [Sat, 17 Dec 2016 15:22:00 +0100] rev 64585
renewed and spread FIXME tags on watering bin interpretation, which got partially lost in 9f089287687b
src/HOL/Library/Multiset.thy