NEWS
changeset 48713 bfc08ce7b7b9
parent 48700 0e36cc70cb3e
child 48722 dad2140c2a15
     1.1 --- a/NEWS	Mon Apr 30 12:14:53 2012 +0200
     1.2 +++ b/NEWS	Mon Apr 30 22:18:39 2012 +1000
     1.3 @@ -180,6 +180,9 @@
     1.4  * Code generation by default implements sets as container type rather
     1.5  than predicates.  INCOMPATIBILITY.
     1.6  
     1.7 +* Records: code generation can be switched off manually with 
     1.8 +declare [[record_coden = false]]. Default remains true.
     1.9 +
    1.10  * HOL-Import: Re-implementation from scratch is faster, simpler, and
    1.11  more scalable.  Requires a proof bundle, which is available as an
    1.12  external component.  Discontinued old (and mostly dead) Importer for