# HG changeset patch
# User wenzelm
# Date 1274966120 -7200
# Node ID 2a5182751151d0b3f5de8b52b503feb63111f484
# Parent  56e1b6976d0e2b43d531206eca005b363c83dec6
constant Rat.normalize needs to be qualified;

diff -r 56e1b6976d0e -r 2a5182751151 NEWS
--- a/NEWS	Thu May 27 13:13:30 2010 +0200
+++ b/NEWS	Thu May 27 15:15:20 2010 +0200
@@ -222,6 +222,9 @@
 * Theory "Rational" renamed to "Rat", for consistency with "Nat",
 "Int" etc.  INCOMPATIBILITY.
 
+* Constant Rat.normalize needs to be qualified.  Minor
+INCOMPATIBILITY.
+
 * New set of rules "ac_simps" provides combined assoc / commute
 rewrites for all interpretations of the appropriate generic locales.
 
diff -r 56e1b6976d0e -r 2a5182751151 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Thu May 27 13:13:30 2010 +0200
+++ b/src/HOL/Rat.thy	Thu May 27 15:15:20 2010 +0200
@@ -1203,4 +1203,7 @@
 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
 by simp
 
+
+hide_const (open) normalize
+
 end