src/ZF/CardinalArith.thy
changeset 13784 b9f6154427a4
parent 13615 449a70d88b38
child 14565 c6dc17aab88a
     1.1 --- a/src/ZF/CardinalArith.thy	Thu Jan 23 09:16:53 2003 +0100
     1.2 +++ b/src/ZF/CardinalArith.thy	Thu Jan 23 10:30:14 2003 +0100
     1.3 @@ -585,14 +585,14 @@
     1.4  (*??WHAT A MESS!*)  
     1.5  apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
     1.6         (assumption | rule refl | erule ltI)+) 
     1.7 -apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
     1.8 +apply (rule_tac i = "xa Un ya" and j = nat in Ord_linear2,
     1.9         simp_all add: Ord_Un Ord_nat)
    1.10  prefer 2 (*case nat le (xa Un ya) *)
    1.11   apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 
    1.12                    le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
    1.13                  ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
    1.14  (*the finite case: xa Un ya < nat *)
    1.15 -apply (rule_tac j = "nat" in lt_trans2)
    1.16 +apply (rule_tac j = nat in lt_trans2)
    1.17   apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
    1.18                    nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
    1.19  apply (simp add: InfCard_def)
    1.20 @@ -645,7 +645,7 @@
    1.21  
    1.22  (*Corollary 10.13 (1), for cardinal multiplication*)
    1.23  lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L"
    1.24 -apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
    1.25 +apply (rule_tac i = K and j = L in Ord_linear_le)
    1.26  apply (typecheck add: InfCard_is_Card Card_is_Ord)
    1.27  apply (rule cmult_commute [THEN ssubst])
    1.28  apply (rule Un_commute [THEN ssubst])
    1.29 @@ -669,7 +669,7 @@
    1.30  done
    1.31  
    1.32  lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L"
    1.33 -apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
    1.34 +apply (rule_tac i = K and j = L in Ord_linear_le)
    1.35  apply (typecheck add: InfCard_is_Card Card_is_Ord)
    1.36  apply (rule cadd_commute [THEN ssubst])
    1.37  apply (rule Un_commute [THEN ssubst])
    1.38 @@ -812,7 +812,7 @@
    1.39  
    1.40  lemma Finite_imp_succ_cardinal_Diff:
    1.41       "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
    1.42 -apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
    1.43 +apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
    1.44  apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
    1.45  apply (simp add: cons_Diff)
    1.46  done