equal
deleted
inserted
replaced
206 val conc = |
206 val conc = |
207 Drule.list_comb (rhs, frees) |
207 Drule.list_comb (rhs, frees) |
208 |> Drule.beta_conv cabs |> Thm.apply cTrueprop |
208 |> Drule.beta_conv cabs |> Thm.apply cTrueprop |
209 fun tacf [prem] = |
209 fun tacf [prem] = |
210 rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} |
210 rewrite_goals_tac ctxt @{thms skolem_def [abs_def]} |
211 THEN resolve_tac [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) |
211 THEN resolve_tac ctxt [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]}) |
212 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1 |
212 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1 |
213 in |
213 in |
214 Goal.prove_internal ctxt [ex_tm] conc tacf |
214 Goal.prove_internal ctxt [ex_tm] conc tacf |
215 |> forall_intr_list frees |
215 |> forall_intr_list frees |
216 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |
216 |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |