src/ZF/Finite.thy
changeset 13784 b9f6154427a4
parent 13615 449a70d88b38
child 14883 ca000a495448
     1.1 --- a/src/ZF/Finite.thy	Thu Jan 23 09:16:53 2003 +0100
     1.2 +++ b/src/ZF/Finite.thy	Thu Jan 23 10:30:14 2003 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  apply (erule Fin_induct)
     1.5  apply (simp add: subset_empty_iff)
     1.6  apply (simp add: subset_cons_iff distrib_simps, safe)
     1.7 -apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
     1.8 +apply (erule_tac b = z in cons_Diff [THEN subst], simp)
     1.9  done
    1.10  
    1.11  lemma Fin_subset: "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)"
    1.12 @@ -158,7 +158,7 @@
    1.13  apply (erule FiniteFun.induct)
    1.14  apply (simp add: subset_empty_iff FiniteFun.intros)
    1.15  apply (simp add: subset_cons_iff distrib_simps, safe)
    1.16 -apply (erule_tac b = "z" in cons_Diff [THEN subst])
    1.17 +apply (erule_tac b = z in cons_Diff [THEN subst])
    1.18  apply (drule spec [THEN mp], assumption)
    1.19  apply (fast intro!: FiniteFun.intros)
    1.20  done