Re: [isabelle] Goal.prove with auto_tac

Hello Steve,

Try using the prop antiquotation, i.e.,

  val t = @{prop "EX x. x = 0"}

The background is that HOL is a logic embedded in Isabelle's
metalogic, and every HOL property needs to be coerced into a meta
justification, for example by using the prop antiquotation.  A more
explicit way to express this would be as follows:

  val t = HOLogic.mk_Trueprop @{term "EX x. x = 0"}


Steve W wrote:
> 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.