# HG changeset patch
# User haftmann
# Date 1207144710 -7200
# Node ID dba7125d0fef1792ea640d5768f6e718e96551c7
# Parent  a329af578d69d63bb17dd6f03a52e87e8ad2988d
explicit instantiation

diff -r a329af578d69 -r dba7125d0fef src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Wed Apr 02 15:58:29 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Wed Apr 02 15:58:30 2008 +0200
@@ -42,8 +42,6 @@
 typedef preal = "{A. cut A}"
   by (blast intro: cut_of_rat [OF zero_less_one])
 
-instance preal :: "{ord, plus, minus, times, inverse, one}" ..
-
 definition
   preal_of_rat :: "rat => preal" where
   "preal_of_rat q = Abs_preal {x::rat. 0 < x & x < q}"
@@ -68,30 +66,41 @@
   inverse_set :: "rat set => rat set" where
   "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
 
+instantiation preal :: "{ord, plus, minus, times, inverse, one}"
+begin
 
-defs (overloaded)
-
+definition
   preal_less_def:
     "R < S == Rep_preal R < Rep_preal S"
 
+definition
   preal_le_def:
     "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
 
+definition
   preal_add_def:
     "R + S == Abs_preal (add_set (Rep_preal R) (Rep_preal S))"
 
+definition
   preal_diff_def:
     "R - S == Abs_preal (diff_set (Rep_preal R) (Rep_preal S))"
 
+definition
   preal_mult_def:
     "R * S == Abs_preal (mult_set (Rep_preal R) (Rep_preal S))"
 
+definition
   preal_inverse_def:
     "inverse R == Abs_preal (inverse_set (Rep_preal R))"
 
+definition
   preal_one_def:
     "1 == preal_of_rat 1"
 
+instance ..
+
+end
+
 
 text{*Reduces equality on abstractions to equality on representatives*}
 declare Abs_preal_inject [simp]