> I guess the general question is, whether it is fine to add the plugin > infrastructure for (most of the) existing commands (e.g., definition, > typedef, record, fun), thus enabling us writing tools that extend the > command’s functionality (be them enabled by default or not).
I am enthusiastically in favour of this proposal. Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
