kleing@15139: For Isabelle2005:
kleing@15139: 
nipkow@15675: - update course material slides to new theory headers (Tobias)
nipkow@15675: 
nipkow@15675: - shell script to convert to new theory headers
nipkow@15310: 
nipkow@15441: - attach additional ML code to consts_code section (Stefan)
nipkow@15441: 
nipkow@15310: - modular generation of ML code with structures (Stefan)
kleing@15139: 
nipkow@15445: - Library/ExecutableSet.thy (Stefan)
nipkow@15310: 
nipkow@15310: - a global "disprove" menu item both as an action and (if it can be done)
nipkow@15310:   as a setting (Stefan & Tjark)
nipkow@15310: 
paulson@15965: - convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias)
paulson@15965: 
nipkow@15424: - update or remove ex/MT (Larry)  
paulson@15330: 
paulson@15412: - Include IsaPlanner? (Larry to co-ordinate)
paulson@15412: 
nipkow@15441: - rules -> iprover (Stefan)
nipkow@15441: 
nipkow@15654: - ball, bex and setsum congruence rules (Tobias & Stefan)
nipkow@15654: 
nipkow@15310: - remove this file (Tobias)