src/HOL/Rat.thy
changeset 37143 2a5182751151
parent 36415 a168ac750096
child 37397 18000f9d783e
     1.1 --- a/src/HOL/Rat.thy	Thu May 27 13:13:30 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Thu May 27 15:15:20 2010 +0200
     1.3 @@ -1203,4 +1203,7 @@
     1.4  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
     1.5  by simp
     1.6  
     1.7 +
     1.8 +hide_const (open) normalize
     1.9 +
    1.10  end