equal
deleted
inserted
replaced
487 termination relations as lexicographic combinations of size measures. |
487 termination relations as lexicographic combinations of size measures. |
488 Usage for (function package) termination proofs: |
488 Usage for (function package) termination proofs: |
489 |
489 |
490 termination |
490 termination |
491 by lexicographic_order |
491 by lexicographic_order |
492 |
|
493 Contributed by Lukas Bulwahn. |
|
494 |
492 |
495 * Records: generalised field-update to take a function on the field |
493 * Records: generalised field-update to take a function on the field |
496 rather than the new value: r(|A := x|) is translated to A_update (K x) r |
494 rather than the new value: r(|A := x|) is translated to A_update (K x) r |
497 The K-combinator that is internally used is called K_record. |
495 The K-combinator that is internally used is called K_record. |
498 INCOMPATIBILITY: Usage of the plain update functions has to be |
496 INCOMPATIBILITY: Usage of the plain update functions has to be |