TODO
author huffman
Fri Sep 16 20:30:44 2005 +0200 (2005-09-16)
changeset 17439 a358da1a0218
parent 16930 8d0daa50f381
child 17471 fa31452b9af6
permissions -rw-r--r--
add header
kleing@15139
     1
For Isabelle2005:
kleing@15139
     2
nipkow@15675
     3
- update course material slides to new theory headers (Tobias)
nipkow@15675
     4
nipkow@15441
     5
- attach additional ML code to consts_code section (Stefan)
nipkow@15441
     6
nipkow@15310
     7
- modular generation of ML code with structures (Stefan)
kleing@15139
     8
nipkow@15445
     9
- Library/ExecutableSet.thy (Stefan)
nipkow@15310
    10
nipkow@15310
    11
- a global "disprove" menu item both as an action and (if it can be done)
nipkow@15310
    12
  as a setting (Stefan & Tjark)
nipkow@15310
    13
paulson@15965
    14
- convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias)
paulson@15965
    15
nipkow@15424
    16
- update or remove ex/MT (Larry)  
paulson@15330
    17
paulson@15412
    18
- Include IsaPlanner? (Larry to co-ordinate)
paulson@15412
    19
nipkow@15441
    20
- rules -> iprover (Stefan)
nipkow@15441
    21
nipkow@15654
    22
- ball, bex and setsum congruence rules (Tobias & Stefan)
nipkow@15654
    23
nipkow@15310
    24
- remove this file (Tobias)