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