equal
deleted
inserted
replaced
143 apply (erule SumE_fst) |
143 apply (erule SumE_fst) |
144 apply (rule replace_type) |
144 apply (rule replace_type) |
145 apply (rule subst_eqtyparg) |
145 apply (rule subst_eqtyparg) |
146 apply (rule comp_rls) |
146 apply (rule comp_rls) |
147 apply (rule_tac [4] SumE_snd) |
147 apply (rule_tac [4] SumE_snd) |
148 apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *}) |
148 apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *}) |
149 done |
149 done |
150 |
150 |
151 text "Axiom of choice. Proof without fst, snd. Harder still!" |
151 text "Axiom of choice. Proof without fst, snd. Harder still!" |
152 schematic_lemma [folded basic_defs]: |
152 schematic_lemma [folded basic_defs]: |
153 assumes "A type" |
153 assumes "A type" |