equal
deleted
inserted
replaced
91 INCOMPATIBILITY. |
91 INCOMPATIBILITY. |
92 |
92 |
93 * Code generation: |
93 * Code generation: |
94 - theory Library/Code_Char_ord provides native ordering of characters |
94 - theory Library/Code_Char_ord provides native ordering of characters |
95 in the target language. |
95 in the target language. |
96 |
96 - commands code_module and code_library are legacy, use export_code instead. |
|
97 - evaluator "SML" and method evaluation are legacy, use evaluator "code" |
|
98 and method eval instead. |
|
99 |
97 * Declare ext [intro] by default. Rare INCOMPATIBILITY. |
100 * Declare ext [intro] by default. Rare INCOMPATIBILITY. |
98 |
101 |
99 * Nitpick: |
102 * Nitpick: |
100 - Added "need" and "total_consts" options. |
103 - Added "need" and "total_consts" options. |
101 - Reintroduced "show_skolems" option by popular demand. |
104 - Reintroduced "show_skolems" option by popular demand. |
130 - New counterexample generator quickcheck[narrowing] enables |
133 - New counterexample generator quickcheck[narrowing] enables |
131 narrowing-based testing. |
134 narrowing-based testing. |
132 It requires that the Glasgow Haskell compiler is installed and |
135 It requires that the Glasgow Haskell compiler is installed and |
133 its location is known to Isabelle with the environment variable |
136 its location is known to Isabelle with the environment variable |
134 ISABELLE_GHC. |
137 ISABELLE_GHC. |
|
138 - Removed quickcheck tester "SML" based on the SML code generator |
|
139 from HOL-Library |
135 |
140 |
136 * Function package: discontinued option "tailrec". |
141 * Function package: discontinued option "tailrec". |
137 INCOMPATIBILITY. Use partial_function instead. |
142 INCOMPATIBILITY. Use partial_function instead. |
138 |
143 |
139 * HOL-Probability: |
144 * HOL-Probability: |