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