doc-src/TutorialI/ToyList/ROOT.ML
author aspinall
Wed, 03 Jan 2007 21:09:13 +0100
changeset 21982 fe30893e50f2
parent 9834 109b11c4e77e
permissions -rw-r--r--
Expose command failure recovery code for top level.

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