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

author | wenzelm |

Mon, 04 Aug 2014 17:55:11 +0200 | |

changeset 57856 | 73c683e09401 |

parent 57855 | 4a5d335a6fc7 |

child 57857 | 4d86378e635f |

tuned;

--- a/NEWS Mon Aug 04 17:53:17 2014 +0200 +++ b/NEWS Mon Aug 04 17:55:11 2014 +0200 @@ -355,9 +355,9 @@ - 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 + - 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, 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 @@ -365,13 +365,13 @@ + 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 + + property that a relator preservers reflexivity is not needed any more Minor INCOMPATIBILITY. - + left_total and left_unique rules are now transfer rules + + 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 + + Domainp does not have to be a separate assumption in relator_domain theorems (=> more natural statement) INCOMPATIBILITY. - registration of code equations is more robust @@ -381,12 +381,12 @@ Potential INCOMPATIBILITY. - eq_onp is always unfolded in respectfulness proof obligation Potential INCOMPATIBILITY. - - unregister lifting setup for Code_Numeral.integer and + - 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 @@ -806,9 +806,8 @@ * 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-Library / theory RBT: various constants and facts are hidden; +lifting setup is unregistered. INCOMPATIBILITY. * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy.