TODO
author paulson
Thu Nov 25 12:39:12 2004 +0100 (2004-11-25)
changeset 15330 630981482718
parent 15317 ebdd193e15ec
child 15346 ac272926fb77
permissions -rw-r--r--
ML
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
  Gfp.ML
paulson@15330
    19
  HOL_lemmas.ML
paulson@15330
    20
  Lfp.ML
paulson@15330
    21
  NatArith.ML
paulson@15330
    22
  Relation_Power.ML
paulson@15330
    23
  Sum_Type.ML
paulson@15330
    24
  Wellfounded_Recursion.ML
paulson@15330
    25
  Wellfounded_Relations.ML
paulson@15330
    26
nipkow@15310
    27
- remove this file (Tobias)