--- a/NEWS Tue Sep 20 11:35:10 2016 +0200
+++ b/NEWS Tue Sep 20 14:51:58 2016 +0200
@@ -276,6 +276,11 @@
* Theory Library/Perm.thy: basic facts about almost everywhere fix
bijections.
+* Theory Library/Normalized_Fraction.thy: allows viewing an element
+of a field of fractions as a normalized fraction (i.e. a pair of
+numerator and denominator such that the two are coprime and the
+denominator is normalized w.r.t. unit factors)
+
* Locale bijection establishes convenient default simp rules
like "inv f (f a) = a" for total bijections.