Translator v0.2 Changelog

• Added support for the sequence enumeration (affects the HolAst and the translator itself)
• Added support for token expressions (only affects the translator)
• Added support for textLiteral, a symbolic literal expression (only affects the translator)
• Added support for the hd operator (only affects the translator)
• Added support for the tl operator (only affects the translator)
• Added support for the len operator (only affects the translator)
• Added support for the sequence concatenation operator (only affects the translator)
• Bugfix in the requirements calculation of the Hol function definition (in the Hol AST). Using a direct recursive call resulted in an error which posed that the function definition contained a mutual recursive dependency, even if it did not. The function itself is now excluded from the requirements list, fixing this issue and allowing for definition of regular recursive functions (and their correct dependency order resolution).

Many thanks to Miguel Ferreira for his help in improving the translator

-- SanderVermolen - 18 Jan 2008