equal
deleted
inserted
replaced
89 differently). |
89 differently). |
90 |
90 |
91 |
91 |
92 *** HOL *** |
92 *** HOL *** |
93 |
93 |
|
94 * Code generator: explicit proof contexts in many ML interfaces. |
|
95 INCOMPATIBILITY. |
|
96 |
94 * Code generator: minimize exported identifiers by default. |
97 * Code generator: minimize exported identifiers by default. |
|
98 Minor INCOMPATIBILITY. |
95 |
99 |
96 * Code generation for SML and OCaml: dropped arcane "no_signatures" option. |
100 * Code generation for SML and OCaml: dropped arcane "no_signatures" option. |
|
101 Minor INCOMPATIBILITY. |
97 |
102 |
98 * Simproc "finite_Collect" is no longer enabled by default, due to |
103 * Simproc "finite_Collect" is no longer enabled by default, due to |
99 spurious crashes and other surprises. Potential INCOMPATIBILITY. |
104 spurious crashes and other surprises. Potential INCOMPATIBILITY. |
100 |
105 |
101 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". |
106 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL". |