doc-src/TutorialI/Trie/ROOT.ML
author haftmann
Sat, 02 Jul 2011 10:37:35 +0200
changeset 43639 9cba66fb109a
parent 10543 8e4307d1207a
permissions -rw-r--r--
correction: do not assume that case const index covered all cases

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