Re: [isabelle] Problems with Logic.mk_implies + compose_tac

On Mon, 2011-07-11 at 11:37 +0200, Holger Gast wrote:
> The short answer is: If you use Goal.prove_internal instead of Goal.prove,
> your approach works just fine. (See the code below.)
>  [...]

Fantastic, thank you very much, Holger. This solved my problems

Kind regards,

Attachment: signature.asc
Description: This is a digitally signed message part

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