changeset 9078 | b8780970d0ed |
parent 8177 | e59e93ad85eb |
child 10834 | a7897aebbffc |
--- a/src/HOL/IMPP/Hoare.ML Fri Jun 16 13:18:55 2000 +0200 +++ b/src/HOL/IMPP/Hoare.ML Fri Jun 16 13:19:15 2000 +0200 @@ -260,9 +260,8 @@ by (cut_facts_tac (premises()) 1); by (induct_tac "n" 1); by (ALLGOALS Clarsimp_tac); -bd card_seteq 1; -by (Asm_simp_tac 1); -be finite_imageI 1; +by (subgoal_tac "G = mgt_call `` U" 1); +by (asm_simp_tac (simpset() addsimps [card_seteq, finite_imageI]) 2); by (Asm_full_simp_tac 1); by (eresolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1); br ballI 1;