doc-src/TutorialI/ToyList2/ROOT.ML
author wenzelm
Sun, 21 Oct 2007 14:21:53 +0200
changeset 25132 dffe405b090d
parent 8745 13b32661dde4
permissions -rw-r--r--
removed obsolete ML bindings;

use_thy "ToyList";