diff -r 6bf380202adb -r 3f3d2ffb5df5 NEWS --- a/NEWS Fri Dec 21 20:58:42 2001 +0100 +++ b/NEWS Fri Dec 21 23:16:17 2001 +0100 @@ -190,6 +190,8 @@ "extend" to promote a fixed record to a record scheme, and "truncate" for the reverse; cf. theorems "xxx.defs", which are *not* declared as simp by default; + - shared operations ("more", "fields", etc.) now need to be always + qualified) --- potential INCOMPATIBILITY; - removed "make_scheme" operations (use "make" with "extend") -- INCOMPATIBILITY; - removed "more" class (simply use "term") -- INCOMPATIBILITY;