equal
deleted
inserted
replaced
176 Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => |
176 Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} => |
177 mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps' |
177 mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps' |
178 inj_map_strongs') |
178 inj_map_strongs') |
179 |> HOLogic.conj_elims ctxt |
179 |> HOLogic.conj_elims ctxt |
180 |> Proof_Context.export names_ctxt ctxt |
180 |> Proof_Context.export names_ctxt ctxt |
181 |> map Thm.close_derivation |
181 |> map (Thm.close_derivation \<^here>) |
182 end; |
182 end; |
183 |
183 |
184 fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _) |
184 fun get_countable_goal_type_name (\<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>Ex\<close>, _) |
185 $ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0 |
185 $ Abs (_, Type (_, [Type (s, _), _]), Const (\<^const_name>\<open>inj_on\<close>, _) $ Bound 0 |
186 $ Const (\<^const_name>\<open>top\<close>, _)))) = s |
186 $ Const (\<^const_name>\<open>top\<close>, _)))) = s |