*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Problems with Logic.mk_implies + compose_tac*From*: Matej Urbas <mu232 at cam.ac.uk>*Date*: Mon, 11 Jul 2011 12:48:27 +0100*Cc*: Holger Gast <gast at informatik.uni-tuebingen.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.1.10.1107111258570.6196@atbroy100.informatik.tu-muenchen.de>*References*: <1310215039.3708.28.camel@toncka.urbas.si> <4E1AC445.9050406@informatik.uni-tuebingen.de> <alpine.LNX.1.10.1107111258570.6196@atbroy100.informatik.tu-muenchen.de>

On Mon, 2011-07-11 at 13:03 +0200, Makarius wrote: > Grepping through the sources (or using hypersearch in jEdit) is indeed > very important to get an idea how common certain operations are. > > Goal.prove_internal shows up very rarely, in special situations or ported > versions of quite old tools (the latter aspect can be seen from the > Mercurial history, if this extra time is spent with it). > > We are getting at an interesting collection of odds and ends of internal > system tools. I maintain that it is possible to ignore all this for > regular applications, and just use the standard system structures around > the Pure rule calculus and its goal format, without lots of workarounds. I see. It makes perfect sense (under the assumption that the definition of 'regular applications' leans favourably and reasonably towards users' requirements). In any case, is it possible to get the same fine-grained control (and exactly the same behaviour) as Holger's proposal using the standard workflow? Best, --- Matej

**Attachment:
signature.asc**

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

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

**Re: [isabelle] Problems with Logic.mk_implies + compose_tac***From:*Holger Gast

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

- Previous by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- 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