explicit definition for "/"
authorhaftmann
Mon Apr 07 15:37:31 2008 +0200 (2008-04-07)
changeset 26564631ce7f6bdc6
parent 26563 420567ad8125
child 26565 522f45a8604e
explicit definition for "/"
src/HOL/Real/PReal.thy
     1.1 --- a/src/HOL/Real/PReal.thy	Mon Apr 07 15:37:30 2008 +0200
     1.2 +++ b/src/HOL/Real/PReal.thy	Mon Apr 07 15:37:31 2008 +0200
     1.3 @@ -93,6 +93,8 @@
     1.4    preal_inverse_def:
     1.5      "inverse R == Abs_preal (inverse_set (Rep_preal R))"
     1.6  
     1.7 +definition "R / S = R * inverse (S\<Colon>preal)"
     1.8 +
     1.9  definition
    1.10    preal_one_def:
    1.11      "1 == preal_of_rat 1"