--- a/src/HOL/Real/PReal.thy Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/PReal.thy Fri Dec 07 15:07:59 2007 +0100
@@ -211,12 +211,20 @@
instance preal :: linorder
by intro_classes (rule preal_le_linear)
-instance preal :: distrib_lattice
- "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
- "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> max"
+instantiation preal :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
+
+definition
+ "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
+
+instance
by intro_classes
(auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
+end
subsection{*Properties of Addition*}