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