[isabelle-dev] copy_bnf

Lars Hupel hupel at in.tum.de
Thu Oct 29 14:12:01 CET 2015


> 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





More information about the isabelle-dev mailing list