src/Doc/Tutorial/Setup.thy
Wed, 23 Dec 2020 23:03:03 +0100 wenzelm avoid multiple uses of the same ML file;
less more (0) tip