Re: [isabelle] match_tac, schematic and bound variables

I see that match_tac is basically part of the classical reasoner. It is for applying rules safely without affecting the proof state. Any significant change in its behaviour would breaks lots of things, but it's conceivable that there's a bug in this example. Or else the documentation isn't quite accurate.

On 12 Aug 2013, at 19:09, Makarius <makarius at> wrote:

> The documentation is also going back to Larry.
> I don't complain about anything he did there many years ago.  One needs to be realistic about what certain parts of a system can do and what not.

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