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