[isabelle] Goal.prove with auto_tac



Hello,

I'm trying to experiment with Goal.prove on a very simple lemma:

ML {*
  let
    val trm = @{term "EX x. x = 0"}
    val ctxt = @{context}
  in
    Goal.prove ctxt [] [] trm (K (auto_tac (clasimpset_of ctxt)))
  end;

*}

Unfortunately, I get an exception saying "instantiate: type conflict". Does
anyone know what I'm doing wrong? I know I could write it as a tactic and
apply it in Isar, but I'm just trying to experiment with Goal.prove.

Regards,
Steve




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