HOL/record: shared operations ("more", "fields", etc.) now need to be
authorwenzelm
Fri Dec 21 23:16:17 2001 +0100 (2001-12-21)
changeset 125873f3d2ffb5df5
parent 12586 6bf380202adb
child 12588 0361fd72f1a7
HOL/record: shared operations ("more", "fields", etc.) now need to be
always qualified;
NEWS
     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;