equal
deleted
inserted
replaced
474 (trailing "_") by default; use '!' option for full details. |
474 (trailing "_") by default; use '!' option for full details. |
475 |
475 |
476 |
476 |
477 *** HOL *** |
477 *** HOL *** |
478 |
478 |
|
479 * Records: generalised field-update to take a function on the field |
|
480 rather than the new value: r(|A := x|) is translated to A_update (K x) r |
|
481 The K-combinator that is internally used is called K_record. |
|
482 INCOMPATIBILITY: Usage of the plain update functions has to be |
|
483 adapted. |
|
484 |
479 * axclass "semiring_0" now contains annihilation axioms |
485 * axclass "semiring_0" now contains annihilation axioms |
480 ("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer |
486 ("x * 0 = 0","0 * x = 0"), which are required for a semiring. Richer |
481 structures do not inherit from semiring_0 anymore, because this property |
487 structures do not inherit from semiring_0 anymore, because this property |
482 is a theorem there, not an axiom. |
488 is a theorem there, not an axiom. |
483 INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but |
489 INCOMPATIBILITY: In instances of semiring_0, there is more to prove, but |