For Isabelle2005: - update course material slides to new theory headers (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) - convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias) - update or remove ex/MT (Larry) - Include IsaPlanner? (Larry to co-ordinate) - rules -> iprover (Stefan) - ball, bex and setsum congruence rules (Tobias & Stefan) - remove this file (Tobias)