equal
deleted
inserted
replaced
212 fun tacf [prem] = |
212 fun tacf [prem] = |
213 rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} |
213 rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} |
214 THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) |
214 THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) |
215 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1 |
215 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1 |
216 in |
216 in |
217 Goal.prove_internal [ex_tm] conc tacf |
217 Goal.prove_internal ctxt [ex_tm] conc tacf |
218 |> forall_intr_list frees |
218 |> forall_intr_list frees |
219 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
219 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
220 |> Thm.varifyT_global |
220 |> Thm.varifyT_global |
221 end |
221 end |
222 |
222 |