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/Real/RealDef.thy
changeset 10648 a8c647cfa31f
parent 10606 e3229a37d53f
child 10752 c4f1bf2acf4c 
--- a/src/HOL/Real/RealDef.thy	Tue Dec 12 11:59:25 2000 +0100
+++ b/src/HOL/Real/RealDef.thy	Tue Dec 12 12:01:19 2000 +0100
@@ -37,7 +37,7 @@
   "R - (S::real) == R + - S"
 
   real_inverse_def
-  "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)"
+  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1r)"
 
   real_divide_def
   "R / (S::real) == R * inverse S"
isabelle