doc-src/TutorialI/Trie/ROOT.ML
author huffman
Wed, 18 Nov 2009 15:01:00 -0800
changeset 33775 7a1518c42c56
parent 10543 8e4307d1207a
permissions -rw-r--r--
cleaned up; factored out fixed-point definition code

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