doc-src/TutorialI/Trie/ROOT.ML
author nipkow
Mon, 09 Mar 2009 09:38:36 +0100
changeset 30372 96d508968153
parent 10543 8e4307d1207a
permissions -rw-r--r--
UN syntax fix

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