TODO
author wenzelm
Fri Jun 17 18:33:21 2005 +0200 (2005-06-17)
changeset 16436 7eb6b6cbd166
parent 16164 6b0d68207c14
child 16930 8d0daa50f381
permissions -rw-r--r--
added type theory: generic theory contexts with unique identity,
arbitrarily typed data, linear and graph development -- a complete
rewrite of code that used to be spread over in sign.ML, theory.ML,
theory_data.ML, pure_thy.ML;
     1 For Isabelle2005:
     2 
     3 - update course material slides to new theory headers (Tobias)
     4 
     5 - shell script to convert to new theory headers
     6 
     7 - attach additional ML code to consts_code section (Stefan)
     8 
     9 - modular generation of ML code with structures (Stefan)
    10 
    11 - Library/ExecutableSet.thy (Stefan)
    12 
    13 - a global "disprove" menu item both as an action and (if it can be done)
    14   as a setting (Stefan & Tjark)
    15 
    16 - convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias)
    17 
    18 - update or remove ex/MT (Larry)  
    19 
    20 - Include IsaPlanner? (Larry to co-ordinate)
    21 
    22 - rules -> iprover (Stefan)
    23 
    24 - ball, bex and setsum congruence rules (Tobias & Stefan)
    25 
    26 - remove this file (Tobias)