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

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 8 16:59:00 CET 2011

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)

More information about the isabelle-dev mailing list