summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kuncar |

Wed, 30 Jul 2014 16:44:54 +0200 | |

changeset 57826 | a01caa7145d4 |

parent 57825 | 58f46c678352 |

child 57827 | abc60f963842 |

NEWS

--- a/NEWS Tue Jul 29 17:13:25 2014 +0200 +++ b/NEWS Wed Jul 30 16:44:54 2014 +0200 @@ -348,6 +348,42 @@ INCOMPATIBILITY. +* Lifting and Transfer: + - a type variable as a raw type is supported + - stronger reflexivity prover + - rep_eq is always generated by lift_definition + - setup for Lifting/Transfer is now automated for BNFs + + holds for BNFs that do not contain a dead variable + + relator_eq, relator_mono, relator_distr, relator_domain, + relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total, + right_unique, right_total, left_unique, left_total are proved + automatically + + definition of a predicator is generated automatically + + simplification rules for a predicator definition are proved + automatically for datatypes + - consolidation of the setup of Lifting/Transfer + + property that a relator preservers reflexivity is not needed any + more + Minor INCOMPATIBILITY. + + left_total and left_unique rules are now transfer rules + (reflexivity_rule attribute not needed anymore) + INCOMPATIBILITY. + + Domainp does not have to be a separate assumption in + relator_domain theorems (=> more natural statement) + INCOMPATIBILITY. + - registration of code equations is more robust + Potential INCOMPATIBILITY. + - respectfulness proof obligation is preprocessed to a more readable + form + Potential INCOMPATIBILITY. + - eq_onp is always unfolded in respectfulness proof obligation + Potential INCOMPATIBILITY. + - unregister lifting setup for Code_Numeral.integer and + Code_Numeral.natural + Potential INCOMPATIBILITY. + - Lifting.invariant -> eq_onp + INCOMPATIBILITY. + * New internal SAT solver "cdclite" that produces models and proof traces. This solver replaces the internal SAT solvers "enumerate" and "dpll". Applications that explicitly used one of these two SAT @@ -767,6 +803,10 @@ * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it is subsumed by session Kleene_Algebra in AFP. +* HOL-Library: RBT.thy: various constants and facts are hidden; + lifting setup is unregistered + INCOMPATIBILITY. + * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. * HOL-Word: bit representations prefer type bool over type bit.