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