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