equal
deleted
inserted
replaced
259 non-recursive definitions. For constants that are not fully parametric |
259 non-recursive definitions. For constants that are not fully parametric |
260 the command will infer conditions on relations (e.g., bi_unique, |
260 the command will infer conditions on relations (e.g., bi_unique, |
261 bi_total, or type class conditions such as "respects 0") sufficient for |
261 bi_total, or type class conditions such as "respects 0") sufficient for |
262 parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for |
262 parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for |
263 some examples. |
263 some examples. |
|
264 |
|
265 * A new preprocessor for the code generator to generate code for algebraic |
|
266 types with lazy evaluation semantics even in call-by-value target languages. |
|
267 See theory HOL-Library.Code_Lazy for the implementation and |
|
268 HOL-Codegenerator_Test.Code_Lazy_Test for examples. |
264 |
269 |
265 * SMT module: |
270 * SMT module: |
266 - The 'smt_oracle' option is now necessary when using the 'smt' method |
271 - The 'smt_oracle' option is now necessary when using the 'smt' method |
267 with a solver other than Z3. INCOMPATIBILITY. |
272 with a solver other than Z3. INCOMPATIBILITY. |
268 - The encoding to first-order logic is now more complete in the |
273 - The encoding to first-order logic is now more complete in the |