src/Pure/Tools/plugin.ML
Mon, 13 Oct 2014 15:45:23 +0200 wenzelm support for named plugins for definitional packages;
less more (0) tip