| author | wenzelm |
| Mon, 05 Sep 2005 17:38:25 +0200 | |
| changeset 17268 | 309288714d9d |
| parent 16930 | 8d0daa50f381 |
| child 17471 | fa31452b9af6 |
| permissions | -rw-r--r-- |
| 15139 | 1 |
For Isabelle2005: |
2 |
||
| 15675 | 3 |
- update course material slides to new theory headers (Tobias) |
4 |
||
| 15441 | 5 |
- attach additional ML code to consts_code section (Stefan) |
6 |
||
| 15310 | 7 |
- modular generation of ML code with structures (Stefan) |
| 15139 | 8 |
|
| 15445 | 9 |
- Library/ExecutableSet.thy (Stefan) |
| 15310 | 10 |
|
11 |
- a global "disprove" menu item both as an action and (if it can be done) |
|
12 |
as a setting (Stefan & Tjark) |
|
13 |
||
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15841
diff
changeset
|
14 |
- convert fast_lin_arith.ML and cooper_dec.ML to use IntInf (Tobias) |
|
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15841
diff
changeset
|
15 |
|
| 15424 | 16 |
- update or remove ex/MT (Larry) |
| 15330 | 17 |
|
| 15412 | 18 |
- Include IsaPlanner? (Larry to co-ordinate) |
19 |
||
| 15441 | 20 |
- rules -> iprover (Stefan) |
21 |
||
| 15654 | 22 |
- ball, bex and setsum congruence rules (Tobias & Stefan) |
23 |
||
| 15310 | 24 |
- remove this file (Tobias) |