# HG changeset patch # User nipkow # Date 1106149524 -3600 # Node ID 8244894d0a4141fa9a953cdd2fcef827a84715b6 # Parent 4f14c151d9f18a580fc124335c0e640f71f9c4c0 *** empty log message *** diff -r 4f14c151d9f1 -r 8244894d0a41 TODO --- a/TODO Tue Jan 18 14:38:20 2005 +0100 +++ b/TODO Wed Jan 19 16:45:24 2005 +0100 @@ -6,9 +6,7 @@ - modular generation of ML code with structures (Stefan) -> Unfortunately when ?s are switched off during building Isabelle this -> broke something inside the datatype package (for Isar I think) - (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)