src/ZF/Ordinal.thy
changeset 13784 b9f6154427a4
parent 13615 449a70d88b38
child 14565 c6dc17aab88a
     1.1 --- a/src/ZF/Ordinal.thy	Thu Jan 23 09:16:53 2003 +0100
     1.2 +++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:30:14 2003 +0100
     1.3 @@ -173,7 +173,7 @@
     1.4  (*There is no set of all ordinals, for then it would contain itself*)
     1.5  lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
     1.6  apply (rule notI)
     1.7 -apply (frule_tac x = "X" in spec)
     1.8 +apply (frule_tac x = X in spec)
     1.9  apply (safe elim!: mem_irrefl)
    1.10  apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
    1.11  apply (simp add: Transset_def)
    1.12 @@ -366,13 +366,13 @@
    1.13  
    1.14  lemma Ord_linear2:
    1.15      "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P"
    1.16 -apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
    1.17 +apply (rule_tac i = i and j = j in Ord_linear_lt)
    1.18  apply (blast intro: leI le_eqI sym ) +
    1.19  done
    1.20  
    1.21  lemma Ord_linear_le:
    1.22      "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P"
    1.23 -apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
    1.24 +apply (rule_tac i = i and j = j in Ord_linear_lt)
    1.25  apply (blast intro: leI le_eqI ) +
    1.26  done
    1.27  
    1.28 @@ -380,7 +380,7 @@
    1.29  by (blast elim!: leE elim: lt_asym)
    1.30  
    1.31  lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i"
    1.32 -by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
    1.33 +by (rule_tac i = i and j = j in Ord_linear2, auto)
    1.34  
    1.35  subsubsection{*Some Rewrite Rules for <, le*}
    1.36  
    1.37 @@ -495,7 +495,7 @@
    1.38  
    1.39  (*Replacing k by succ(k') yields the similar rule for le!*)
    1.40  lemma Un_least_lt: "[| i<k;  j<k |] ==> i Un j < k"
    1.41 -apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
    1.42 +apply (rule_tac i = i and j = j in Ord_linear_le)
    1.43  apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) 
    1.44  done
    1.45  
    1.46 @@ -513,7 +513,7 @@
    1.47  
    1.48  (*Replacing k by succ(k') yields the similar rule for le!*)
    1.49  lemma Int_greatest_lt: "[| i<k;  j<k |] ==> i Int j < k"
    1.50 -apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
    1.51 +apply (rule_tac i = i and j = j in Ord_linear_le)
    1.52  apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
    1.53  done
    1.54