src/HOL/Rat.thy
changeset 36415 a168ac750096
parent 36409 d323e7773aa8
child 37143 2a5182751151
     1.1 --- a/src/HOL/Rat.thy	Tue Apr 27 09:49:36 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Tue Apr 27 09:49:40 2010 +0200
     1.3 @@ -440,7 +440,9 @@
     1.4  next
     1.5    fix q r :: rat
     1.6    show "q / r = q * inverse r" by (simp add: divide_rat_def)
     1.7 -qed (simp add: rat_number_expand, simp add: rat_number_collapse)
     1.8 +next
     1.9 +  show "inverse 0 = (0::rat)" by (simp add: rat_number_expand, simp add: rat_number_collapse)
    1.10 +qed
    1.11  
    1.12  end
    1.13