TODO
author paulson
Wed Dec 08 10:28:05 2004 +0100 (2004-12-08)
changeset 15386 06757406d8cf
parent 15346 ac272926fb77
child 15391 797ed46d724b
permissions -rw-r--r--
converted Lfp to new-style theory
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)
webertj@15317
    15
paulson@15330
    16
- eliminate the last remaining old-style theories (Larry):  
paulson@15330
    17
  Datatype_Universe.ML
paulson@15330
    18
  HOL_lemmas.ML
paulson@15330
    19
  NatArith.ML
paulson@15330
    20
  Relation_Power.ML
paulson@15330
    21
  Sum_Type.ML
paulson@15386
    22
  
paulson@15386
    23
- update or remove ex/MT (Larry? Tobias?)  
paulson@15330
    24
nipkow@15310
    25
- remove this file (Tobias)