src/ZF/Cardinal.thy

 lemma nat_lepoll_imp_le [rule_format]:
      "m:nat ==> ALL n: nat. m \<lesssim> n --> m le n"
 apply (induct_tac m)
 apply (blast intro!: nat_0_le)
 apply (rule ballI)
-apply (erule_tac n = "n" in natE)
+apply (erule_tac n = n in natE)
 apply (simp (no_asm_simp) add: lepoll_def inj_def)
 apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
 done
 
 lemma nat_eqpoll_iff: "[| m:nat; n: nat |] ==> m \<approx> n <-> m = n"

 apply (subgoal_tac "EX u. u:A")
 apply (erule exE)
 apply (rule Diff_sing_eqpoll [THEN revcut_rl])
 prefer 2 apply assumption
 apply assumption
-apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
 apply (rule Fin.consI, blast)
 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
 (*Now for the lemma assumed above*)
 apply (unfold eqpoll_def)
 apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])

 apply (unfold Finite_def)
 apply (case_tac "a:A")
 apply (subgoal_tac [2] "A-{a}=A", auto)
 apply (rule_tac x = "succ (n) " in bexI)
 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
-apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
+apply (drule_tac a = a and b = n in cons_eqpoll_cong)
 apply (auto dest: mem_irrefl)
 done
 
 (*Sidi Ehmety.  And the contrapositive of this says
    [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)

 apply (rule_tac P =  "x:Z" in case_split_thm)
  txt{*x:Z case*}
  apply (drule_tac x = x in bspec, assumption)
  apply (blast elim: mem_irrefl mem_asym)
 txt{*other case*} 
-apply (drule_tac x = "Z" in spec, blast) 
+apply (drule_tac x = Z in spec, blast) 
 done
 
 lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
 apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
 apply (unfold well_ord_def)