src/HOL/MicroJava/J/Example.thy
Sun, 20 Nov 2011 21:05:23 +0100 wenzelm eliminated obsolete "standard";
less more (0) -30 -10 -1 tip