changeset 31643 | b040f1679f77 |
parent 31626 | fe35b72b9ef0 |
child 31720 | d1ac3f3b2f54 |
child 31723 | f5cafe803b55 |
--- a/NEWS Mon Jun 15 16:13:04 2009 +0200 +++ b/NEWS Mon Jun 15 16:13:19 2009 +0200 @@ -40,6 +40,9 @@ * Implementation of quickcheck using generic code generator; default generators are provided for all suitable HOL types, records and datatypes. +* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions +Set.Pow_def and Set.image_def. INCOMPATIBILITY. + *** ML ***