equal
deleted
inserted
replaced
13 'code_library', 'consts_code', 'types_code' have been discontinued. |
13 'code_library', 'consts_code', 'types_code' have been discontinued. |
14 Use commands of the generic code generator instead. INCOMPATIBILITY. |
14 Use commands of the generic code generator instead. INCOMPATIBILITY. |
15 |
15 |
16 * Redundant attribute 'code_inline' has been discontinued. Use |
16 * Redundant attribute 'code_inline' has been discontinued. Use |
17 'code_unfold' instead. INCOMPATIBILITY. |
17 'code_unfold' instead. INCOMPATIBILITY. |
|
18 |
|
19 * Sort constraints are now propagated in simultaneous statements, just |
|
20 like type constraints. INCOMPATIBILITY in rare situations, where |
|
21 distinct sorts used to be assigned accidentally. For example: |
|
22 |
|
23 lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" |
|
24 |
|
25 lemma "P (x::'a)" and "Q (y::'a::bar)" |
|
26 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
|
27 |
18 |
28 |
19 |
29 |
20 *** HOL *** |
30 *** HOL *** |
21 |
31 |
22 * Clarified attribute "mono_set": pure declararation without modifying |
32 * Clarified attribute "mono_set": pure declararation without modifying |