lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
For Isabelle2005:
- update course material slides to new theory format (Tobias)
- attach additional ML code to consts_code section (Stefan)
- modular generation of ML code with structures (Stefan)
- Library/ExecutableSet.thy (Stefan)
- a global "disprove" menu item both as an action and (if it can be done)
as a setting (Stefan & Tjark)
- check/establish conformity of HTML files to (some version of) the HTML
language specification (cf. http://validator.w3.org/) (Tjark, or anyone
who is interested)
- update or remove ex/MT (Larry)
- Include IsaPlanner? (Larry to co-ordinate)
- update LaTeXsugar, remove references to future Isabelle2005 etc. (Gerwin)
- rules -> iprover (Stefan)
- remove this file (Tobias)