doc-src/TutorialI/Trie/ROOT.ML

fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function

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