equal
deleted
inserted
replaced
22 * Global versions of theorems stemming from classes do not carry |
22 * Global versions of theorems stemming from classes do not carry |
23 a parameter prefix any longer. INCOMPATIBILITY. |
23 a parameter prefix any longer. INCOMPATIBILITY. |
24 |
24 |
25 * Dropped "locale (open)". INCOMPATBILITY. |
25 * Dropped "locale (open)". INCOMPATBILITY. |
26 |
26 |
27 * Command 'interpretation' no longer attempts to simplify goal. |
27 * Interpretation commands no longer attempt to simplify goal. |
28 INCOMPATIBILITY: in rare situations the generated goal differs. Use |
28 INCOMPATIBILITY: in rare situations the generated goal differs. Use |
29 methods intro_locales and unfold_locales to clarify. |
29 methods intro_locales and unfold_locales to clarify. |
|
30 |
|
31 * Interpretation commands no longer accept interpretation attributes. |
|
32 INCOMPATBILITY. |
30 |
33 |
31 * Command 'instance': attached definitions no longer accepted. |
34 * Command 'instance': attached definitions no longer accepted. |
32 INCOMPATIBILITY, use proper 'instantiation' target. |
35 INCOMPATIBILITY, use proper 'instantiation' target. |
33 |
36 |
34 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |
37 * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. |