[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
brianh at cs.pdx.edu
Tue Feb 8 17:58:49 CET 2011
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.
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
More information about the isabelle-dev