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/PReal.thy
changeset 26564 631ce7f6bdc6
parent 26511 dba7125d0fef
child 26806 40b411ec05aa 
--- a/src/HOL/Real/PReal.thy	Mon Apr 07 15:37:30 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Apr 07 15:37:31 2008 +0200
@@ -93,6 +93,8 @@
   preal_inverse_def:
     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
 
+definition "R / S = R * inverse (S\<Colon>preal)"
+
 definition
   preal_one_def:
     "1 == preal_of_rat 1"
isabelle