src/ZF/Finite.thy
changeset 13269 3ba9be497c33
parent 13203 fac77a839aa2
child 13328 703de709a64b
     1.1 --- a/src/ZF/Finite.thy	Mon Jul 01 18:16:18 2002 +0200
     1.2 +++ b/src/ZF/Finite.thy	Tue Jul 02 13:28:08 2002 +0200
     1.3 @@ -151,9 +151,7 @@
     1.4  done
     1.5  
     1.6  lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
     1.7 -apply (erule FiniteFun.induct, simp)
     1.8 -apply simp
     1.9 -done
    1.10 +by (erule FiniteFun.induct, simp, simp)
    1.11  
    1.12  lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
    1.13  
    1.14 @@ -175,8 +173,7 @@
    1.15  
    1.16  lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
    1.17  apply (erule Fin.induct)
    1.18 - apply (simp add: FiniteFun.intros)
    1.19 -apply clarify
    1.20 + apply (simp add: FiniteFun.intros, clarify)
    1.21  apply (case_tac "a:b")
    1.22   apply (rotate_tac -1)
    1.23   apply (simp add: cons_absorb)