doc-src/TutorialI/Trie/ROOT.ML
author huffman
Wed, 24 Dec 2008 13:16:26 -0800
changeset 29170 dad3933c88dd
parent 10543 8e4307d1207a
permissions -rw-r--r--
clean up lemmas about exp

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