equal
deleted
inserted
replaced
339 first a is simplified to b, and then f b is simplified to g. If |
339 first a is simplified to b, and then f b is simplified to g. If |
340 possible we abstract b from g arriving at "let x = b in h x", |
340 possible we abstract b from g arriving at "let x = b in h x", |
341 otherwise we unfold the let and arrive at g. The simproc can be |
341 otherwise we unfold the let and arrive at g. The simproc can be |
342 enabled/disabled by the reference use_let_simproc. Potential |
342 enabled/disabled by the reference use_let_simproc. Potential |
343 INCOMPATIBILITY since simplification is more powerful by default. |
343 INCOMPATIBILITY since simplification is more powerful by default. |
|
344 |
|
345 * Classical reasoning: the meson method now accepts theorems as arguments. |
344 |
346 |
345 |
347 |
346 *** HOLCF *** |
348 *** HOLCF *** |
347 |
349 |
348 * HOLCF: discontinued special version of 'constdefs' (which used to |
350 * HOLCF: discontinued special version of 'constdefs' (which used to |