src/HOL/UNITY/Simple/Lift.thy
changeset 14378 69c4d5997669
parent 13812 91713a1915ee
child 16184 80617b8d33c5
     1.1 --- a/src/HOL/UNITY/Simple/Lift.thy	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/UNITY/Simple/Lift.thy	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -215,13 +215,13 @@
     1.4  lemma moving_up: "Lift \<in> Always moving_up"
     1.5  apply (rule AlwaysI, force) 
     1.6  apply (unfold Lift_def, constrains)
     1.7 -apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq)
     1.8 +apply (auto dest: order_le_imp_less_or_eq simp add: add1_zle_eq)
     1.9  done
    1.10  
    1.11  lemma moving_down: "Lift \<in> Always moving_down"
    1.12  apply (rule AlwaysI, force) 
    1.13  apply (unfold Lift_def, constrains)
    1.14 -apply (blast dest: zle_imp_zless_or_eq)
    1.15 +apply (blast dest: order_le_imp_less_or_eq)
    1.16  done
    1.17  
    1.18  lemma bounded: "Lift \<in> Always bounded"
    1.19 @@ -290,7 +290,7 @@
    1.20      "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))    
    1.21               LeadsTo ((closed \<inter> goingup \<inter> Req n)  \<union> 
    1.22                        (closed \<inter> goingdown \<inter> Req n))"
    1.23 -by (auto intro!: subset_imp_LeadsTo elim!: int_neqE)
    1.24 +by (auto intro!: subset_imp_LeadsTo simp add: linorder_neq_iff)
    1.25  
    1.26  (*lift_2*)
    1.27  lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))