doc-src/TutorialI/Trie/ROOT.ML
author haftmann
Mon, 06 Nov 2006 16:28:37 +0100
changeset 21196 42ee69856dd0
parent 10543 8e4307d1207a
permissions -rw-r--r--
(adjustions)

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