NEWS
changeset 30740 2d3ae5a7edb2
parent 30706 e20227b5e6a3
child 30741 9e23e3ea7edd
     1.1 --- a/NEWS	Fri Mar 27 10:05:12 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 27 10:05:13 2009 +0100
     1.3 @@ -498,10 +498,9 @@
     1.4  resulting ML value/function/datatype constructor binding in place.
     1.5  All occurrences of @{code} with a single ML block are generated
     1.6  simultaneously.  Provides a generic and safe interface for
     1.7 -instrumentalizing code generation.  See HOL/ex/Code_Antiq for a toy
     1.8 -example, or HOL/Complex/ex/ReflectedFerrack for a more ambitious
     1.9 -application.  In future you ought refrain from ad-hoc compiling
    1.10 -generated SML code on the ML toplevel.  Note that (for technical
    1.11 +instrumentalizing code generation.  See HOL/Decision_Procs/Ferrack for
    1.12 +a more ambitious application.  In future you ought refrain from ad-hoc
    1.13 +compiling generated SML code on the ML toplevel.  Note that (for technical
    1.14  reasons) @{code} cannot refer to constants for which user-defined
    1.15  serializations are set.  Refer to the corresponding ML counterpart
    1.16  directly in that cases.