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'
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and