doc-src/TutorialI/Trie/ROOT.ML
author haftmann
Tue, 23 Oct 2007 11:48:08 +0200
changeset 25152 bfde2f8c0f63
parent 10543 8e4307d1207a
permissions -rw-r--r--
partially localized

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