src/HOL/Lattices.thy
changeset 22384 33a46e6c7f04
parent 22168 627e7aee1b82
child 22422 ee19cdb07528
     1.1 --- a/src/HOL/Lattices.thy	Fri Mar 02 12:38:58 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Fri Mar 02 15:43:15 2007 +0100
     1.3 @@ -37,13 +37,13 @@
     1.4  
     1.5  lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
     1.6  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
     1.7 - apply(blast intro:trans)
     1.8 + apply(blast intro: order_trans)
     1.9  apply simp
    1.10  done
    1.11  
    1.12  lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    1.13  apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
    1.14 - apply(blast intro:trans)
    1.15 + apply(blast intro: order_trans)
    1.16  apply simp
    1.17  done
    1.18  
    1.19 @@ -51,7 +51,7 @@
    1.20  by(blast intro: inf_greatest)
    1.21  
    1.22  lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.23 -by(blast intro: trans)
    1.24 +by(blast intro: order_trans)
    1.25  
    1.26  lemma le_inf_iff [simp]:
    1.27   "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    1.28 @@ -70,13 +70,13 @@
    1.29  
    1.30  lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.31  apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
    1.32 - apply(blast intro:trans)
    1.33 + apply(blast intro: order_trans)
    1.34  apply simp
    1.35  done
    1.36  
    1.37  lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    1.38  apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
    1.39 - apply(blast intro:trans)
    1.40 + apply(blast intro: order_trans)
    1.41  apply simp
    1.42  done
    1.43  
    1.44 @@ -84,7 +84,7 @@
    1.45  by(blast intro: sup_least)
    1.46  
    1.47  lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.48 -by(blast intro: trans)
    1.49 +by(blast intro: order_trans)
    1.50  
    1.51  lemma ge_sup_conv[simp]:
    1.52   "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"