doc-src/TutorialI/Trie/ROOT.ML
author paulson
Fri, 03 Sep 2004 10:26:39 +0200
changeset 15176 2fd60846f485
parent 10543 8e4307d1207a
permissions -rw-r--r--
listrel operator for lifting relations to lists

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