equal
deleted
inserted
replaced
35 |
35 |
36 *** HOL *** |
36 *** HOL *** |
37 |
37 |
38 * Code generation for records: more idiomatic representation of record types. |
38 * Code generation for records: more idiomatic representation of record types. |
39 Warning: records are not covered by ancient SML code generation any longer. |
39 Warning: records are not covered by ancient SML code generation any longer. |
40 INCOMPATIBILITY. |
40 INCOMPATIBILITY. In cases of need, a suitable rep_datatype declaration |
|
41 helps to succeed then: |
|
42 |
|
43 record 'a foo = ... |
|
44 ... |
|
45 rep_datatype foo_ext ... |
41 |
46 |
42 * Session Imperative_HOL: revamped, corrected dozens of inadequacies. |
47 * Session Imperative_HOL: revamped, corrected dozens of inadequacies. |
43 INCOMPATIBILITY. |
48 INCOMPATIBILITY. |
44 |
49 |
45 * Quickcheck in locales considers interpretations of that locale for |
50 * Quickcheck in locales considers interpretations of that locale for |