1
2
(* use "../settings.ML";*)
3
set quick_and_dirty;
4
use_thy "Trie1";
5
use_thy "Trie2";
6
use_thy "Trie3";