changeset 25705 | 45a2ffc5911e |
parent 25664 | 156660ab8a39 |
child 25712 | f488a37cfad4 |
--- a/NEWS Tue Dec 18 22:21:42 2007 +0100 +++ b/NEWS Wed Dec 19 16:32:12 2007 +0100 @@ -49,6 +49,10 @@ and makes them available separately. See "HOL/ex/Induction_Scheme.thy" for examples, +* Records. Removed K_record, and replaced it by pure lambda term +%x. c. The simplifier setup is now more robust against eta +expansion. +INCOMPATIBILITY: in cases explicitly referring to K_record. *** System ***