Re: [isabelle] Proving with Goal.prove



On Fri, Oct 1, 2010 at 3:05 AM, Cezary Kaliszyk
<cezarykaliszyk at gmail.com> wrote:
>
> The following does work:
>
>  val {prop,...} = Thm.rep_thm st
>  val t = Goal.prove ctxt [] [] (Logic.unprotect
> (Logic.strip_assums_concl prop)) (fn _ => tac)
>
> But the above is somehow very low-level, if you want to look at
> subparts of the goal in a tactic
> in a convenient way you may want to have a look at the Subgoal.FOCUS
> family of combinators.
>

If I understand correctly, does Logic.unprotect remove the prop marker
from the main conclusion (conclusion of prop)? Is the concl of a focus
supposed to be the main conclusion, but with the prop marker removed?

Thanks.

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.