NEWS
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 ***