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



On Mon, 11 Jul 2011, Matej Urbas wrote:

I see. It makes perfect sense (under the assumption that the definition of 'regular applications' leans favourably and reasonably towards users' requirements).

Yes it does. These things have taken a certain form over many years. It is unwise to ignore all the experience behind it. By doing this the "canonical way", it is easier to get them right, and easier to read and maintain. All the obvious things ...


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?

You still did not explain what you are trying to do exactly. I was about to disprove your assumptions.

There are *rare* situations where one needs to step outside the standard framework, e.g. when implementing new infrastructure. Empirically it is very unlikely that this is the situation here, unless you prove it otherwise.


	Makarius





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