[isabelle] Proving with Goal.prove

Hello again,

I'm trying another example with Goal.prove, but it can't seem to
discharge the proof goal. I must have done something wrong:

ML {*

fun foo ctxt st =
    val {prop,...} = Thm.rep_thm st
    val tac = auto_tac (clasimpset_of ctxt)
    val t = Goal.prove ctxt [] [] prop
      (fn _ => tac)
    tac st


lemma lem1: "EX x y. x = y"
apply (tactic {* foo @{context} *})

Does the value prop not contain the goal of lem1? If not, how can the
goal for the current goal state be retrieved?

Thanks again!


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