Re: [isabelle] match_tac, schematic and bound variables

Am 12/08/2013 22:39, schrieb Lawrence Paulson:
> 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.

The term "match" has precisely the definition you quote in the documentation,
and that should be the specifiation of anything called "match". If the
implementation does not conform, it should be fixed. I agree this may be hard in
this case and it is not a top priority. Alternatively the documentation should
carry a warning.


> Larry
> 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.