--- a/TODO Mon May 16 09:35:05 2005 +0200
+++ b/TODO Mon May 16 10:29:15 2005 +0200
@@ -13,6 +13,8 @@
- 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)
@@ -23,8 +25,6 @@
- ball, bex and setsum congruence rules (Tobias & Stefan)
-- use IntInf.int (Steven)
-
- html generation: somtimes lemma names and whole lemmas are missing.
See http://afp.sourceforge.net/browser_info/current/HOL/HOL-Complex/Integration/SetsumThms.html
(Markus?)