src/ZF/OrderType.thy
changeset 46821 ff6b0c1087f2
parent 46820 c656222c4dc1
child 46841 49b91b716cbe
     1.1 --- a/src/ZF/OrderType.thy	Tue Mar 06 15:15:49 2012 +0000
     1.2 +++ b/src/ZF/OrderType.thy	Tue Mar 06 16:06:52 2012 +0000
     1.3 @@ -533,7 +533,7 @@
     1.4  apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
     1.5  done
     1.6  
     1.7 -lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
     1.8 +lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k \<longleftrightarrow> j<k"
     1.9  by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
    1.10  
    1.11  lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
    1.12 @@ -607,13 +607,13 @@
    1.13                   Union_eq_UN [symmetric] Limit_Union_eq)
    1.14  done
    1.15  
    1.16 -lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
    1.17 +lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 \<longleftrightarrow> i=0 & j=0"
    1.18  apply (erule trans_induct3 [of j])
    1.19  apply (simp_all add: oadd_Limit)
    1.20  apply (simp add: Union_empty_iff Limit_def lt_def, blast)
    1.21  done
    1.22  
    1.23 -lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
    1.24 +lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) \<longleftrightarrow> 0<i | 0<j"
    1.25  by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
    1.26  
    1.27  lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
    1.28 @@ -661,7 +661,7 @@
    1.29  lemma oadd_le_mono: "[| i' \<le> i;  j' \<le> j |] ==> i'++j' \<le> i++j"
    1.30  by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
    1.31  
    1.32 -lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k <-> j \<le> k"
    1.33 +lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j \<le> i++k \<longleftrightarrow> j \<le> k"
    1.34  by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
    1.35  
    1.36  lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"