equal
deleted
inserted
replaced
72 and type constructors. |
72 and type constructors. |
73 |
73 |
74 |
74 |
75 *** HOL *** |
75 *** HOL *** |
76 |
76 |
|
77 * Improved infrastructure for term evaluation using code generator |
|
78 techniques, in particular static evaluation conversions. |
|
79 |
77 * String.literal is a type, but not a datatype. INCOMPATIBILITY. |
80 * String.literal is a type, but not a datatype. INCOMPATIBILITY. |
78 |
81 |
79 * Renamed lemmas: |
82 * Renamed lemmas: |
80 expand_fun_eq -> fun_eq_iff |
83 expand_fun_eq -> fun_eq_iff |
81 expand_set_eq -> set_eq_iff |
84 expand_set_eq -> set_eq_iff |
82 set_ext -> set_eqI |
85 set_ext -> set_eqI |
|
86 INCOMPATIBILITY. |
83 |
87 |
84 * Renamed class eq and constant eq (for code generation) to class equal |
88 * Renamed class eq and constant eq (for code generation) to class equal |
85 and constant equal, plus renaming of related facts and various tuning. |
89 and constant equal, plus renaming of related facts and various tuning. |
86 INCOMPATIBILITY. |
90 INCOMPATIBILITY. |
87 |
91 |