# HG changeset patch
# User haftmann
# Date 1272354580 -7200
# Node ID a168ac750096dc2cf4988d0e7db06b7baed78d6b
# Parent  a19ba9bbc8dcd3cf59d854e44226d2d9c663518e
explicit is better than implicit

diff -r a19ba9bbc8dc -r a168ac750096 src/HOL/Rat.thy
--- 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