doc-src/TutorialI/Misc/Plus.thy
Sat, 11 Mar 2006 17:30:35 +0100 wenzelm renamed plus to add;
less more (0) -1 tip