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