--- 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.
--- 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