# HG changeset patch # User haftmann # Date 1248678073 -7200 # Node ID 420108dd7dfe27ef97dc30db131139b0559721f2 # Parent 2f3d65d15149f60d380ea66034c58eb8e8d1e7c2 NEWS diff -r 2f3d65d15149 -r 420108dd7dfe NEWS --- a/NEWS Sun Jul 26 22:33:32 2009 +0200 +++ b/NEWS Mon Jul 27 09:01:13 2009 +0200 @@ -31,7 +31,7 @@ * New quickcheck implementation using new code generator. -* New type class boolean_algebra. +* New class "boolean_algebra". * Refinements to lattices classes: - added boolean_algebra type class @@ -40,6 +40,19 @@ - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci) - renamed ACI to inf_sup_aci + - class "complete_lattice" moved to separate theory "complete_lattice"; + corresponding constants renamed: + + Set.Inf ~> Complete_Lattice.Inf + Set.Sup ~> Complete_Lattice.Sup + Set.INFI ~> Complete_Lattice.INFI + Set.SUPR ~> Complete_Lattice.SUPR + Set.Inter ~> Complete_Lattice.Inter + Set.Union ~> Complete_Lattice.Union + Set.INTER ~> Complete_Lattice.INTER + Set.UNION ~> Complete_Lattice.UNION + + INCOMPATIBILITY. * Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,