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

[Brian Huffman]

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
>