# HG changeset patch
# User wenzelm
# Date 1126974297 -7200
# Node ID fa31452b9af6dd5266badfaee423752e83151a40
# Parent  6e9d910c38372c44ffbf3ac5ef955b6bab4d0832
tuned;

diff -r 6e9d910c3837 -r fa31452b9af6 TODO
--- a/TODO	Sat Sep 17 18:11:30 2005 +0200
+++ b/TODO	Sat Sep 17 18:24:57 2005 +0200
@@ -2,10 +2,6 @@
 
 - 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)
@@ -17,8 +13,6 @@
 
 - Include IsaPlanner? (Larry to co-ordinate)
 
-- rules -> iprover (Stefan)
-
 - ball, bex and setsum congruence rules (Tobias & Stefan)
 
 - remove this file (Tobias)