[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Gerwin Klein]

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.

Cheers,
Gerwin

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.
>> Larry
>> 
>> 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
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>