equal
deleted
inserted
replaced
16 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
16 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
17 interface instead. |
17 interface instead. |
18 |
18 |
19 |
19 |
20 *** Pure *** |
20 *** Pure *** |
|
21 |
|
22 * Different bookkeeping for code equations: |
|
23 a) On theory merge, the last set of code equations for a particular constant |
|
24 is taken (in accordance with the policy applied by other parts of the |
|
25 code generator framework). |
|
26 b) Code equations stemming from explicit declarations (e.g. code attribute) |
|
27 gain priority over default code equations stemming from definition, primrec, |
|
28 fun etc. |
|
29 INCOMPATIBILITY. |
21 |
30 |
22 * Global versions of theorems stemming from classes do not carry |
31 * Global versions of theorems stemming from classes do not carry |
23 a parameter prefix any longer. INCOMPATIBILITY. |
32 a parameter prefix any longer. INCOMPATIBILITY. |
24 |
33 |
25 * Dropped "locale (open)". INCOMPATBILITY. |
34 * Dropped "locale (open)". INCOMPATBILITY. |