summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 57856 | 73c683e09401 |

parent 57833 | 2c2bae3da1c2 |

child 57869 | 9665f79a7181 |

1.1 --- a/NEWS Mon Aug 04 17:53:17 2014 +0200 1.2 +++ b/NEWS Mon Aug 04 17:55:11 2014 +0200 1.3 @@ -355,9 +355,9 @@ 1.4 - a type variable as a raw type is supported 1.5 - stronger reflexivity prover 1.6 - rep_eq is always generated by lift_definition 1.7 - - setup for Lifting/Transfer is now automated for BNFs 1.8 + - setup for Lifting/Transfer is now automated for BNFs 1.9 + holds for BNFs that do not contain a dead variable 1.10 - + relator_eq, relator_mono, relator_distr, relator_domain, 1.11 + + relator_eq, relator_mono, relator_distr, relator_domain, 1.12 relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total, 1.13 right_unique, right_total, left_unique, left_total are proved 1.14 automatically 1.15 @@ -365,13 +365,13 @@ 1.16 + simplification rules for a predicator definition are proved 1.17 automatically for datatypes 1.18 - consolidation of the setup of Lifting/Transfer 1.19 - + property that a relator preservers reflexivity is not needed any 1.20 + + property that a relator preservers reflexivity is not needed any 1.21 more 1.22 Minor INCOMPATIBILITY. 1.23 - + left_total and left_unique rules are now transfer rules 1.24 + + left_total and left_unique rules are now transfer rules 1.25 (reflexivity_rule attribute not needed anymore) 1.26 INCOMPATIBILITY. 1.27 - + Domainp does not have to be a separate assumption in 1.28 + + Domainp does not have to be a separate assumption in 1.29 relator_domain theorems (=> more natural statement) 1.30 INCOMPATIBILITY. 1.31 - registration of code equations is more robust 1.32 @@ -381,12 +381,12 @@ 1.33 Potential INCOMPATIBILITY. 1.34 - eq_onp is always unfolded in respectfulness proof obligation 1.35 Potential INCOMPATIBILITY. 1.36 - - unregister lifting setup for Code_Numeral.integer and 1.37 + - unregister lifting setup for Code_Numeral.integer and 1.38 Code_Numeral.natural 1.39 Potential INCOMPATIBILITY. 1.40 - Lifting.invariant -> eq_onp 1.41 INCOMPATIBILITY. 1.42 - 1.43 + 1.44 * New internal SAT solver "cdclite" that produces models and proof 1.45 traces. This solver replaces the internal SAT solvers "enumerate" and 1.46 "dpll". Applications that explicitly used one of these two SAT 1.47 @@ -806,9 +806,8 @@ 1.48 * HOL-Library: removed theory src/HOL/Library/Kleene_Algebra.thy; it 1.49 is subsumed by session Kleene_Algebra in AFP. 1.50 1.51 -* HOL-Library: RBT.thy: various constants and facts are hidden; 1.52 - lifting setup is unregistered 1.53 - INCOMPATIBILITY. 1.54 +* HOL-Library / theory RBT: various constants and facts are hidden; 1.55 +lifting setup is unregistered. INCOMPATIBILITY. 1.56 1.57 * HOL-Cardinals: new theory src/HOL/Cardinals/Ordinal_Arithmetic.thy. 1.58