# HG changeset patch
# User haftmann
# Date 1207575451 -7200
# Node ID 631ce7f6bdc6223fd87be64addcb2421d6e246d7
# Parent  420567ad81251e3d8773db2f1febab505f152d5f
explicit definition for "/"

diff -r 420567ad8125 -r 631ce7f6bdc6 src/HOL/Real/PReal.thy
--- 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"