*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] match_tac, schematic and bound variables*From*: Makarius <makarius at sketis.net>*Date*: Sat, 17 Aug 2013 15:05:38 +0200 (CEST)*In-reply-to*: <5209C6A7.9030804@in.tum.de>*References*: <5208CE6E.6090808@in.tum.de> <alpine.LNX.2.00.1308121808590.20188@macbroy21.informatik.tu-muenchen.de> <52091156.5000305@in.tum.de> <alpine.LNX.2.00.1308122008290.4538@macbroy21.informatik.tu-muenchen.de> <425305E4-DB7A-4B0E-BD30-A8E1CC1E059E@cam.ac.uk> <5209C6A7.9030804@in.tum.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 13 Aug 2013, Tobias Nipkow wrote:

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 thedocumentation, and that should be the specifiation of anything called"match". If the implementation does not conform, it should be fixed. Iagree this may be hard in this case and it is not a top priority.Alternatively the documentation should carry a warning.

Makarius

**References**:**[isabelle] match_tac, schematic and bound variables***From:*Lars Noschinski

**Re: [isabelle] match_tac, schematic and bound variables***From:*Makarius

**Re: [isabelle] match_tac, schematic and bound variables***From:*Tobias Nipkow

**Re: [isabelle] match_tac, schematic and bound variables***From:*Makarius

**Re: [isabelle] match_tac, schematic and bound variables***From:*Lawrence Paulson

**Re: [isabelle] match_tac, schematic and bound variables***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] string and altstring
- Next by Date: Re: [isabelle] List.span
- Previous by Thread: Re: [isabelle] match_tac, schematic and bound variables
- Next by Thread: Re: [isabelle] match_tac, schematic and bound variables
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list