src/ZF/Finite.thy

 (*Every subset of a finite set is finite.*)
 lemma Fin_subset_lemma [rule_format]: "b: Fin(A) ==> \<forall>z. z<=b --> z: Fin(A)"
 apply (erule Fin_induct)
 apply (simp add: subset_empty_iff)
 apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
+apply (erule_tac b = z in cons_Diff [THEN subst], simp)
 done
 
 lemma Fin_subset: "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)"
 by (blast intro: Fin_subset_lemma)
 

 lemma FiniteFun_subset_lemma [rule_format]:
      "b: A-||>B ==> ALL z. z<=b --> z: A-||>B"
 apply (erule FiniteFun.induct)
 apply (simp add: subset_empty_iff FiniteFun.intros)
 apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst])
+apply (erule_tac b = z in cons_Diff [THEN subst])
 apply (drule spec [THEN mp], assumption)
 apply (fast intro!: FiniteFun.intros)
 done
 
 lemma FiniteFun_subset: "[| c<=b;  b: A-||>B |] ==> c: A-||>B"