Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quotient_Examples/Quotient_Rat.thy
changeset 59867 58043346ca64
parent 59557 ebd8ecacfba6
child 61076 bdc1e2f0a86a 
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Tue Mar 31 21:54:32 2015 +0200
@@ -161,7 +161,7 @@
   apply auto
   done
 
-instantiation rat :: field_inverse_zero begin
+instantiation rat :: field begin
 
 fun rat_inverse_raw where
   "rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
isabelle