equal
deleted
inserted
replaced
1 Isabelle NEWS -- history user-relevant changes |
1 Isabelle NEWS -- history user-relevant changes |
2 ============================================== |
2 ============================================== |
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
|
6 |
|
7 *** General *** |
|
8 |
|
9 * Rule attributes in local theory declarations (e.g. locale or class) |
|
10 are now statically evaluated: the resulting theorem is stored instead |
|
11 of the original expression. INCOMPATIBILITY in rare situations, where |
|
12 the historic accident of dynamic re-evaluation in interpretations |
|
13 etc. was exploited. |
|
14 |
6 |
15 |
7 *** Pure *** |
16 *** Pure *** |
8 |
17 |
9 * Obsolete command 'types' has been discontinued. Use 'type_synonym' |
18 * Obsolete command 'types' has been discontinued. Use 'type_synonym' |
10 instead. INCOMPATIBILITY. |
19 instead. INCOMPATIBILITY. |
22 |
31 |
23 lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
32 lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
24 |
33 |
25 lemma "P (x::'a)" and "Q (y::'a::bar)" |
34 lemma "P (x::'a)" and "Q (y::'a::bar)" |
26 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
35 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
27 |
|
28 |
36 |
29 |
37 |
30 *** HOL *** |
38 *** HOL *** |
31 |
39 |
32 * Session HOL-Word: Discontinued many redundant theorems specific to type |
40 * Session HOL-Word: Discontinued many redundant theorems specific to type |