src/ZF/CardinalArith.ML

 
 (*** Finite sets ***)
 
 Goal "n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
 by (etac nat_induct 1);
-by (simp_tac (simpset() addsimps (eqpoll_0_iff::Fin.intrs)) 1);
+by (simp_tac (simpset() addsimps eqpoll_0_iff::Fin.intrs) 1);
 by (Clarify_tac 1);
 by (subgoal_tac "EX u. u:A" 1);
 by (etac exE 1);
 by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1);
 by (assume_tac 2);