NEWS
changeset 38537 6a78c972de27
parent 38535 9f64860c6ec0
child 38545 e30c782329bf
     1.1 --- a/NEWS	Tue Aug 17 16:44:24 2010 +0200
     1.2 +++ b/NEWS	Wed Aug 18 15:01:57 2010 +0200
     1.3 @@ -37,7 +37,12 @@
     1.4  
     1.5  * Code generation for records: more idiomatic representation of record types.
     1.6  Warning: records are not covered by ancient SML code generation any longer.
     1.7 -INCOMPATIBILITY.
     1.8 +INCOMPATIBILITY.  In cases of need, a suitable rep_datatype declaration
     1.9 +helps to succeed then:
    1.10 +
    1.11 +  record 'a foo = ...
    1.12 +  ...
    1.13 +  rep_datatype foo_ext ...
    1.14  
    1.15  * Session Imperative_HOL: revamped, corrected dozens of inadequacies.
    1.16  INCOMPATIBILITY.