src/ZF/Int_ZF.thy
changeset 46841 49b91b716cbe
parent 46821 ff6b0c1087f2
child 46953 2b6e55924af3
     1.1 --- a/src/ZF/Int_ZF.thy	Tue Mar 06 17:01:37 2012 +0000
     1.2 +++ b/src/ZF/Int_ZF.thy	Thu Mar 08 16:43:29 2012 +0000
     1.3 @@ -707,7 +707,7 @@
     1.4  apply auto
     1.5  done
     1.6  
     1.7 -lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
     1.8 +lemma zless_trans [trans]: "[| x $< y; y $< z |] ==> x $< z"
     1.9  apply (subgoal_tac "intify (x) $< intify (z) ")
    1.10  apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
    1.11  apply auto
    1.12 @@ -750,19 +750,19 @@
    1.13  apply (blast intro: zless_trans)
    1.14  done
    1.15  
    1.16 -lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
    1.17 +lemma zle_trans [trans]: "[| x $<= y; y $<= z |] ==> x $<= z"
    1.18  apply (subgoal_tac "intify (x) $<= intify (z) ")
    1.19  apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
    1.20  apply auto
    1.21  done
    1.22  
    1.23 -lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
    1.24 +lemma zle_zless_trans [trans]: "[| i $<= j; j $< k |] ==> i $< k"
    1.25  apply (auto simp add: zle_def)
    1.26  apply (blast intro: zless_trans)
    1.27  apply (simp add: zless_def zdiff_def zadd_def)
    1.28  done
    1.29  
    1.30 -lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
    1.31 +lemma zless_zle_trans [trans]: "[| i $< j; j $<= k |] ==> i $< k"
    1.32  apply (auto simp add: zle_def)
    1.33  apply (blast intro: zless_trans)
    1.34  apply (simp add: zless_def zdiff_def zminus_def)