*To*: Matej Urbas <mu232 at cam.ac.uk>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Makarius <makarius at sketis.net>*Date*: Sun, 10 Jul 2011 21:43:15 +0200 (CEST)*Cc*: Isabelle Users Mailing List <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1310215039.3708.28.camel@toncka.urbas.si>*References*: <1310215039.3708.28.camel@toncka.urbas.si>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Sat, 9 Jul 2011, Matej Urbas wrote:

I want to 'replace' the current subgoal sg1 with sg2. Therefore I make a meta-implication and prove it with 'Goal.prove': val intert = Logic.mk_implies (sg2, sg1) val interThm = Goal.prove ctxt [] [] inter1 (K ((auto_tac (clasimpset_of ctxt)) THEN (ALLGOALS (Intuitionistic.prover_tac ctxt NONE))))

The next step is to use interThm in 'compose_tac', which is applied on the original goal sg1: compose_tac (false, interThm, 1) i which fails.

Makarius

**Follow-Ups**:**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Matej Urbas

**References**:**[isabelle] Problems with Logic.mk_implies + compose_tac***From:*Matej Urbas

- Previous by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Next by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Previous by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Thread: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list