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



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
Description: This is a digitally signed message part



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