doc-src/TutorialI/ToyList2/ROOT.ML
author wenzelm
Wed, 17 Jun 2009 17:07:26 +0200
changeset 31687 0d2f700fe5e7
parent 8745 13b32661dde4
permissions -rw-r--r--
more detailed start_timing/end_timing;

use_thy "ToyList";