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 <[email protected]> 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 > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
