# HG changeset patch
# User paulson
# Date 1021646891 -7200
# Node ID a40db0418145179300a853227615348a31562280
# Parent  eca781285662042b11b1f5886c6d09d3158382b6
unsymbolize

diff -r eca781285662 -r a40db0418145 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Fri May 17 16:47:24 2002 +0200
+++ b/src/ZF/CardinalArith.thy	Fri May 17 16:48:11 2002 +0200
@@ -52,16 +52,16 @@
 (*** The following really belong in Order ***)
 
 lemma subset_ord_iso_Memrel:
-     "\<lbrakk>f: ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f: ord_iso(A,Memrel(A),C,r)"
+     "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 
 apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 
 apply (simp add: right_comp_id) 
 done
 
 lemma restrict_ord_iso:
-     "\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
-       trans[A](r)\<rbrakk>
-      \<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
+     "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
+       trans[A](r) |]
+      ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
 apply (frule ltD) 
 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 
 apply (frule ord_iso_restrict_pred, assumption) 
@@ -70,21 +70,21 @@
 done
 
 lemma restrict_ord_iso2:
-     "\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
-       j < i; trans[A](r)\<rbrakk>
-      \<Longrightarrow> converse(restrict(converse(f), j)) 
+     "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a \<in> A; 
+       j < i; trans[A](r) |]
+      ==> converse(restrict(converse(f), j)) 
           \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
 by (blast intro: restrict_ord_iso ord_iso_sym ltI)
 
 (*** The following really belong in OrderType ***)
 
-lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
+lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
 apply (erule trans_induct3 [of j])
 apply (simp_all add: oadd_Limit)
 apply (simp add: Union_empty_iff Limit_def lt_def, blast)
 done
 
-lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
+lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
 
 lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"
@@ -94,7 +94,7 @@
 apply (blast intro: succ_leI oadd_le_mono)
 done
 
-lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)"
+lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
 apply (simp add: oadd_Limit)
 apply (frule Limit_has_1 [THEN ltD])
 apply (rule increasing_LimitI)