[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
gerwin.klein at nicta.com.au
Tue Feb 8 22:38:09 CET 2011
I don't mind either way, but I'd like to point out that the _tac instantiations are everything but out of fashion. I'm fully aware that they are bad style, rely on dynamic names, etc, but there is no way around them if you write apply style.
On 09/02/2011, at 3:58 AM, Brian Huffman wrote:
> The *_tac-style instantiation might be out of fashion, but the same
> parsing rules for indexnames are also used with the "where" attribute,
> which is still quite useful.
> - Brian
> On Tue, Feb 8, 2011 at 7:59 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> Obviously this proposal would involve a significant incompatibility. It may not even be very relevant any more, as this sort of instantiation is rather out of fashion. But it is worth a discussion.
>> Begin forwarded message:
>>> I would propose to simplify the parsing rules to work like this: Any
>>> variable name with index 0 can be referred to without a question mark
>>> or dot, and a dot is always required for indices other than 0.
>>> x, ?x and ?x.0 parse as ("x", 0)
>>> x0, ?x0 and ?x0.0 parse as ("x0", 0)
>>> x2, ?x2 and ?x2.0 parse as ("x2", 0)
>>> ?x.2 parses as ("x", 2)
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev