doc-src/TutorialI/Trie/ROOT.ML
author haftmann
Tue, 12 Jan 2010 16:27:42 +0100
changeset 34891 99b9a6290446
parent 10543 8e4307d1207a
permissions -rw-r--r--
code certificates as integral part of code generation

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