doc-src/TutorialI/ToyList/ROOT.ML
author haftmann
Wed, 13 Jan 2010 10:18:45 +0100
changeset 34894 fadbdd350dd1
parent 9834 109b11c4e77e
permissions -rw-r--r--
corrected error messages; tuned

use "../settings.ML";
use_thy "ToyList";