20 months ago haftmann [Sun, 08 Oct 2017 22:28:20 +0200] rev 66804
avoid name clashes on interpretation of abstract locales
NEWS src/HOL/Analysis/Bochner_Integration.thy src/HOL/Analysis/Bounded_Linear_Function.thy src/HOL/Analysis/Caratheodory.thy src/HOL/Analysis/Cartesian_Euclidean_Space.thy src/HOL/Analysis/Determinants.thy src/HOL/Analysis/Linear_Algebra.thy src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy src/HOL/Computational_Algebra/Formal_Power_Series.thy src/HOL/Groups_Big.thy src/HOL/Inequalities.thy src/HOL/Library/Groups_Big_Fun.thy src/HOL/Probability/Probability_Mass_Function.thy src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:20 +0200] rev 66803
avoid trivial definition
NEWS src/HOL/GCD.thy src/HOL/Number_Theory/Totient.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:20 +0200] rev 66802
canonical introduction and destruction rules for pairwise
src/HOL/Set.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:20 +0200] rev 66801
avoid fact name clashes
NEWS src/HOL/Code_Numeral.thy src/HOL/Divides.thy src/HOL/Number_Theory/Quadratic_Reciprocity.thy src/HOL/Word/Word_Miscellaneous.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66800
spelling and tuned whitespace
src/HOL/Divides.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66799
tuned
src/HOL/Computational_Algebra/Polynomial.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66798
fundamental property of division by units
src/HOL/Euclidean_Division.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66797
removed mere toy example from library
src/HOL/Library/Function_Growth.thy src/HOL/Library/Library.thy src/HOL/ROOT src/HOL/ex/Function_Growth.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66796
tuned proofs
src/HOL/GCD.thy

20 months ago haftmann [Sun, 08 Oct 2017 22:28:19 +0200] rev 66795
dropped dead code
src/HOL/Nat_Transfer.thy src/HOL/Tools/legacy_transfer.ML