Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
explicit is better than implicit
authorhaftmann
Tue, 27 Apr 2010 09:49:40 +0200
changeset 36415 a168ac750096
parent 36414 a19ba9bbc8dc
child 36416 9459be72b89e
explicit is better than implicit
src/HOL/Rat.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle