tidied for new card_seteq
authorpaulson
Fri Jun 16 13:19:15 2000 +0200 (2000-06-16)
changeset 9078b8780970d0ed
parent 9077 5bf9b0d6df8a
child 9079 8e9b7095bf59
tidied for new card_seteq
src/HOL/IMPP/Hoare.ML
     1.1 --- a/src/HOL/IMPP/Hoare.ML	Fri Jun 16 13:18:55 2000 +0200
     1.2 +++ b/src/HOL/IMPP/Hoare.ML	Fri Jun 16 13:19:15 2000 +0200
     1.3 @@ -260,9 +260,8 @@
     1.4  by (cut_facts_tac (premises()) 1);
     1.5  by (induct_tac "n" 1);
     1.6  by  (ALLGOALS Clarsimp_tac);
     1.7 -bd  card_seteq 1;
     1.8 -by    (Asm_simp_tac 1);
     1.9 -be   finite_imageI 1;
    1.10 +by  (subgoal_tac "G = mgt_call `` U" 1);
    1.11 +by   (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2);
    1.12  by  (Asm_full_simp_tac 1);
    1.13  by  (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
    1.14  br  ballI 1;