src/HOL/Orderings.thy
changeset 25193 e2e1a4b00de3
parent 25103 1ee419a5a30f
child 25207 d58c14280367
     1.1 --- a/src/HOL/Orderings.thy	Thu Oct 25 16:57:57 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Oct 25 19:27:50 2007 +0200
     1.3 @@ -685,17 +685,22 @@
     1.4  
     1.5  subsection {* Transitivity reasoning *}
     1.6  
     1.7 -lemma ord_le_eq_trans: "a <= b ==> b = c ==> a <= c"
     1.8 -by (rule subst)
     1.9 +context ord
    1.10 +begin
    1.11  
    1.12 -lemma ord_eq_le_trans: "a = b ==> b <= c ==> a <= c"
    1.13 -by (rule ssubst)
    1.14 +lemma ord_le_eq_trans: "a \<le> b \<Longrightarrow> b = c \<Longrightarrow> a \<le> c"
    1.15 +  by (rule subst)
    1.16  
    1.17 -lemma ord_less_eq_trans: "a < b ==> b = c ==> a < c"
    1.18 -by (rule subst)
    1.19 +lemma ord_eq_le_trans: "a = b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
    1.20 +  by (rule ssubst)
    1.21  
    1.22 -lemma ord_eq_less_trans: "a = b ==> b < c ==> a < c"
    1.23 -by (rule ssubst)
    1.24 +lemma ord_less_eq_trans: "a < b \<Longrightarrow> b = c \<Longrightarrow> a < c"
    1.25 +  by (rule subst)
    1.26 +
    1.27 +lemma ord_eq_less_trans: "a = b \<Longrightarrow> b < c \<Longrightarrow> a < c"
    1.28 +  by (rule ssubst)
    1.29 +
    1.30 +end
    1.31  
    1.32  lemma order_less_subst2: "(a::'a::order) < b ==> f b < (c::'c::order) ==>
    1.33    (!!x y. x < y ==> f x < f y) ==> f a < c"