src/HOL/Real/PReal.thy
changeset 25571 c9e39eafc7a0
parent 25502 9200b36280c0
child 26511 dba7125d0fef
     1.1 --- a/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:56 2007 +0100
     1.2 +++ b/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:59 2007 +0100
     1.3 @@ -211,12 +211,20 @@
     1.4  instance preal :: linorder
     1.5    by intro_classes (rule preal_le_linear)
     1.6  
     1.7 -instance preal :: distrib_lattice
     1.8 -  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
     1.9 -  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
    1.10 +instantiation preal :: distrib_lattice
    1.11 +begin
    1.12 +
    1.13 +definition
    1.14 +  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
    1.15 +
    1.16 +definition
    1.17 +  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
    1.18 +
    1.19 +instance
    1.20    by intro_classes
    1.21      (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
    1.22  
    1.23 +end
    1.24  
    1.25  subsection{*Properties of Addition*}
    1.26