doc-src/TutorialI/Trie/ROOT.ML
author berghofe
Fri, 28 Sep 2001 16:42:58 +0200
changeset 11620 54e2f4c8c3cb
parent 10543 8e4307d1207a
permissions -rw-r--r--
Added \ttlbrack and \ttrbrack.

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