# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1474375918 -7200
# Node ID c9bba9dba73b19bcf231db707dd1c5f33c13aab0
# Parent  d184a824aa6386042f568a6b5faacb5079e8de27
NEWS: Normalized_Fraction.thy

diff -r d184a824aa63 -r c9bba9dba73b NEWS
--- 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.