TODO

update -> use

+
−For Isabelle2005:
+
−
+
−- update course material slides to new theory headers (Tobias)
+
−
+
−- shell script to convert to new theory headers
+
−
+
−- 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)