equal
deleted
inserted
replaced
1400 \<longrightarrow> (\<forall>t. P A {mgf t})" |
1400 \<longrightarrow> (\<forall>t. P A {mgf t})" |
1401 using finU uA |
1401 using finU uA |
1402 apply - |
1402 apply - |
1403 apply (induct_tac "n") |
1403 apply (induct_tac "n") |
1404 apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})") |
1404 apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})") |
1405 apply (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *}) |
1405 apply (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *}) |
1406 apply simp |
1406 apply simp |
1407 apply (erule finite_imageI) |
1407 apply (erule finite_imageI) |
1408 apply (simp add: MGF_asm ax_derivs_asm) |
1408 apply (simp add: MGF_asm ax_derivs_asm) |
1409 apply (rule MGF_asm) |
1409 apply (rule MGF_asm) |
1410 apply (rule ballI) |
1410 apply (rule ballI) |