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 definition for "/"
authorhaftmann
Mon, 07 Apr 2008 15:37:31 +0200
changeset 26564 631ce7f6bdc6
parent 26563 420567ad8125
child 26565 522f45a8604e
explicit definition for "/"
src/HOL/Real/PReal.thy file | annotate | diff | comparison | revisions 
--- 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