[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 =
  let
    val {prop,...} = Thm.rep_thm st
    val tac = auto_tac (clasimpset_of ctxt)
    val t = Goal.prove ctxt [] [] prop
      (fn _ => tac)
  in
    tac st
  end;

*}

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!

John





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