src/HOL/Lubs.thy
changeset 51520 e9b361845809
parent 46509 c4b2ec379fdd
     1.1 --- a/src/HOL/Lubs.thy	Tue Mar 26 12:20:53 2013 +0100
     1.2 +++ b/src/HOL/Lubs.thy	Tue Mar 26 12:20:54 2013 +0100
     1.3 @@ -94,4 +94,10 @@
     1.4  lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
     1.5    unfolding ubs_def isLub_def by (rule leastPD2)
     1.6  
     1.7 +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
     1.8 +  apply (frule isLub_isUb)
     1.9 +  apply (frule_tac x = y in isLub_isUb)
    1.10 +  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
    1.11 +  done
    1.12 +
    1.13  end