TODO
author paulson
Wed Dec 15 10:19:19 2004 +0100 (2004-12-15)
changeset 15412 7f373e478a5a
parent 15391 797ed46d724b
child 15414 d945f05e75a2
permissions -rw-r--r--
*** empty log message ***
kleing@15139
     1
For Isabelle2005:
kleing@15139
     2
nipkow@15310
     3
- update course material slides to new theory format (Tobias)
nipkow@15310
     4
nipkow@15310
     5
- modular generation of ML code with structures (Stefan)
kleing@15139
     6
nipkow@15310
     7
- finding rewrite rules based on PG subterm selection (Tobias)
nipkow@15310
     8
nipkow@15310
     9
- a global "disprove" menu item both as an action and (if it can be done)
nipkow@15310
    10
  as a setting (Stefan & Tjark)
nipkow@15310
    11
webertj@15317
    12
- check/establish conformity of HTML files to (some version of) the HTML
webertj@15317
    13
  language specification (cf. http://validator.w3.org/) (Tjark, or anyone
webertj@15317
    14
  who is interested)
paulson@15412
    15
  
paulson@15412
    16
- fix the inductive definition bug (Larry): Equations in the intro rules can make proofs fail. Perhaps the critical proof could "protect" the initial equations e.g. by disjoining False, and removing this later.
paulson@15386
    17
  
paulson@15386
    18
- update or remove ex/MT (Larry? Tobias?)  
paulson@15330
    19
paulson@15412
    20
- Include IsaPlanner? (Larry to co-ordinate)
paulson@15412
    21
nipkow@15310
    22
- remove this file (Tobias)