src/HOL/Lattices.thy
changeset 25482 4ed49eccb1eb
parent 25382 72cfe89f7b21
child 25510 38c15efe603b
     1.1 --- a/src/HOL/Lattices.thy	Wed Nov 28 09:01:34 2007 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Nov 28 09:01:37 2007 +0100
     1.3 @@ -39,7 +39,8 @@
     1.4    assumes "a \<sqsubseteq> x"
     1.5    shows "a \<sqinter> b \<sqsubseteq> x"
     1.6  proof (rule order_trans)
     1.7 -  show "a \<sqinter> b \<sqsubseteq> a" and "a \<sqsubseteq> x" using assms by simp
     1.8 +  from assms show "a \<sqsubseteq> x" .
     1.9 +  show "a \<sqinter> b \<sqsubseteq> a" by simp 
    1.10  qed
    1.11  lemmas (in -) [rule del] = le_infI1
    1.12  
    1.13 @@ -47,7 +48,8 @@
    1.14    assumes "b \<sqsubseteq> x"
    1.15    shows "a \<sqinter> b \<sqsubseteq> x"
    1.16  proof (rule order_trans)
    1.17 -  show "a \<sqinter> b \<sqsubseteq> b" and "b \<sqsubseteq> x" using assms by simp
    1.18 +  from assms show "b \<sqsubseteq> x" .
    1.19 +  show "a \<sqinter> b \<sqsubseteq> b" by simp
    1.20  qed
    1.21  lemmas (in -) [rule del] = le_infI2
    1.22