equal
deleted
inserted
replaced
8 |
8 |
9 * Prover IDE (PIDE) improvements: |
9 * Prover IDE (PIDE) improvements: |
10 |
10 |
11 - markup for bound variables |
11 - markup for bound variables |
12 - markup for types of term variables (e.g. displayed as tooltips) |
12 - markup for types of term variables (e.g. displayed as tooltips) |
|
13 |
|
14 * Updated and extended reference manuals ("isar-ref" and |
|
15 "implementation"); reduced remaining material in old "ref" manual. |
13 |
16 |
14 * Rule attributes in local theory declarations (e.g. locale or class) |
17 * Rule attributes in local theory declarations (e.g. locale or class) |
15 are now statically evaluated: the resulting theorem is stored instead |
18 are now statically evaluated: the resulting theorem is stored instead |
16 of the original expression. INCOMPATIBILITY in rare situations, where |
19 of the original expression. INCOMPATIBILITY in rare situations, where |
17 the historic accident of dynamic re-evaluation in interpretations |
20 the historic accident of dynamic re-evaluation in interpretations |