doc-src/TutorialI/Misc/document/AdvancedInd.tex
Mon, 23 Jun 2008 15:26:48 +0200 wenzelm updated generated file;
Thu, 01 Nov 2007 20:20:19 +0100 nipkow recdef -> fun
Tue, 16 Oct 2007 17:07:40 +0200 wenzelm updated;
less more (0) -30 -10 -3 tip