equal
deleted
inserted
replaced
9 * Rule attributes in local theory declarations (e.g. locale or class) |
9 * Rule attributes in local theory declarations (e.g. locale or class) |
10 are now statically evaluated: the resulting theorem is stored instead |
10 are now statically evaluated: the resulting theorem is stored instead |
11 of the original expression. INCOMPATIBILITY in rare situations, where |
11 of the original expression. INCOMPATIBILITY in rare situations, where |
12 the historic accident of dynamic re-evaluation in interpretations |
12 the historic accident of dynamic re-evaluation in interpretations |
13 etc. was exploited. |
13 etc. was exploited. |
|
14 |
|
15 * Commands 'lemmas' and 'theorems' allow local variables using 'for' |
|
16 declaration, and results are standardized before being stored. Thus |
|
17 old-style "standard" after instantiation or composition of facts |
|
18 becomes obsolete. Minor INCOMPATIBILITY, due to potential change of |
|
19 indices of schematic variables. |
14 |
20 |
15 |
21 |
16 *** Pure *** |
22 *** Pure *** |
17 |
23 |
18 * Obsolete command 'types' has been discontinued. Use 'type_synonym' |
24 * Obsolete command 'types' has been discontinued. Use 'type_synonym' |