TODO
author kleing
Mon May 16 09:35:05 2005 +0200 (2005-05-16)
changeset 15964 f2074e12d1d4
parent 15841 29bda008409e
child 15965 f422f8283491
permissions -rw-r--r--
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
kleing@15139
     1
For Isabelle2005:
kleing@15139
     2
nipkow@15675
     3
- update course material slides to new theory headers (Tobias)
nipkow@15675
     4
nipkow@15675
     5
- shell script to convert to new theory headers
nipkow@15310
     6
nipkow@15441
     7
- attach additional ML code to consts_code section (Stefan)
nipkow@15441
     8
nipkow@15310
     9
- modular generation of ML code with structures (Stefan)
kleing@15139
    10
nipkow@15445
    11
- Library/ExecutableSet.thy (Stefan)
nipkow@15310
    12
nipkow@15310
    13
- a global "disprove" menu item both as an action and (if it can be done)
nipkow@15310
    14
  as a setting (Stefan & Tjark)
nipkow@15310
    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
kleing@15419
    20
- update LaTeXsugar, remove references to future Isabelle2005 etc. (Gerwin)
kleing@15414
    21
nipkow@15441
    22
- rules -> iprover (Stefan)
nipkow@15441
    23
nipkow@15654
    24
- ball, bex and setsum congruence rules (Tobias & Stefan)
nipkow@15654
    25
nipkow@15738
    26
- use IntInf.int (Steven)
nipkow@15738
    27
nipkow@15701
    28
- html generation: somtimes lemma names and whole lemmas are missing.
nipkow@15701
    29
  See http://afp.sourceforge.net/browser_info/current/HOL/HOL-Complex/Integration/SetsumThms.html
nipkow@15701
    30
  (Markus?)
nipkow@15701
    31
nipkow@15838
    32
- Allow sorts in typedef:  typedef ('a::mysort)t = ...
nipkow@15838
    33
  (low priority)
nipkow@15838
    34
nipkow@15310
    35
- remove this file (Tobias)