NEWS
changeset 12587 3f3d2ffb5df5
parent 12564 226873bffa3a
child 12597 14822e4436bf
     1.1 --- a/NEWS	Fri Dec 21 20:58:42 2001 +0100
     1.2 +++ b/NEWS	Fri Dec 21 23:16:17 2001 +0100
     1.3 @@ -190,6 +190,8 @@
     1.4      "extend" to promote a fixed record to a record scheme, and
     1.5      "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*
     1.6      declared as simp by default;
     1.7 +  - shared operations ("more", "fields", etc.) now need to be always
     1.8 +    qualified) --- potential INCOMPATIBILITY;
     1.9    - removed "make_scheme" operations (use "make" with "extend") --
    1.10      INCOMPATIBILITY;
    1.11    - removed "more" class (simply use "term") -- INCOMPATIBILITY;