doc-src/TutorialI/Trie/ROOT.ML
author haftmann
Fri, 06 Mar 2009 14:51:18 +0100
changeset 30300 aa44d67eea16
parent 10543 8e4307d1207a
permissions -rw-r--r--
corrected slip in NEWS

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