NEWS
changeset 30741 9e23e3ea7edd
parent 30728 f0aeca99b5d9
parent 30740 2d3ae5a7edb2
child 30845 9a887484de53
     1.1 --- a/NEWS	Fri Mar 27 09:58:48 2009 +0100
     1.2 +++ b/NEWS	Fri Mar 27 10:12:55 2009 +0100
     1.3 @@ -502,10 +502,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.