equal
deleted
inserted
replaced
72 and type constructors. |
72 and type constructors. |
73 |
73 |
74 |
74 |
75 *** HOL *** |
75 *** HOL *** |
76 |
76 |
|
77 * Dropped old primrec package. INCOMPATIBILITY. |
|
78 |
77 * Improved infrastructure for term evaluation using code generator |
79 * Improved infrastructure for term evaluation using code generator |
78 techniques, in particular static evaluation conversions. |
80 techniques, in particular static evaluation conversions. |
79 |
81 |
80 * String.literal is a type, but not a datatype. INCOMPATIBILITY. |
82 * String.literal is a type, but not a datatype. INCOMPATIBILITY. |
81 |
83 |
82 * Renamed lemmas: |
84 * Renamed lemmas: |
83 expand_fun_eq -> fun_eq_iff |
85 expand_fun_eq -> fun_eq_iff |
84 expand_set_eq -> set_eq_iff |
86 expand_set_eq -> set_eq_iff |
85 set_ext -> set_eqI |
87 set_ext -> set_eqI |