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
perfectly.

Kind regards,
---
Matej

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



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