doc-src/TutorialI/ToyList2/ROOT.ML
author wenzelm
Thu, 07 Sep 2000 20:57:22 +0200
changeset 9901 09a142decdda
parent 8745 13b32661dde4
permissions -rw-r--r--
avoid handle_error (better msgs);

use_thy "ToyList";