1.1 --- a/NEWS	Wed Jul 02 07:11:57 2008 +0200
     1.2 +++ b/NEWS	Wed Jul 02 07:12:17 2008 +0200
     1.3 @@ -15,8 +15,20 @@
     1.4  
     1.5  * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
     1.6  
     1.7 +* New ML antiquotation 'code': takes constant as argument, generates
     1.8 +corresponding code in background and inserts name of the corresponding resulting
     1.9 +ML value/function/datatype constructor binding in place.  All occurences of 'code'
    1.10 +with a single ML block are generated simultaneously.
    1.11 +Provides a generic and safe interface for instrumentalizing code generation.
    1.12 +See HOL/ex/Code_Antiq for a toy example, or HOL/Complex/ex/ReflectedFerrack
    1.13 +for a more ambitious application.  In future you ought refrain from
    1.14 +ad-hoc compiling generated SML code on the ML toplevel.
    1.15 +Note that (for technical reasons) 'code' cannot refer to constants for which
    1.16 +user-defined serializations are set.  Refer to the corresponding ML counterpart
    1.17 +directly in that cases.
    1.18 +
    1.19  * Removed exotic 'token_translation' command.  INCOMPATIBILITY, use ML
    1.20 -interface instead.
    1.21 +interface instead. 
    1.22  
    1.23  
    1.24  *** Document preparation ***
    1.25 @@ -32,7 +44,10 @@
    1.26  Complex_Main.thy remain as they are.
    1.27  
    1.28  * New image HOL-Plain provides a minimal HOL with the most important tools
    1.29 -available (inductive, datatype, primrec, codegen, ...).
    1.30 +available (inductive, datatype, primrec, ...).  By convention the corresponding
    1.31 +theory Plain should be ancestor of every further (library) theory.  Some library
    1.32 +theories now have ancestor Plain (instead of Main), thus theory Main
    1.33 +occasionally has to be imported explicitly.
    1.34  
    1.35  * Methods "case_tac" and "induct_tac" now refer to the very same rules
    1.36  as the structured Isar versions "cases" and "induct", cf. the
    1.37 @@ -66,7 +81,7 @@
    1.38  
    1.39  
    1.40  *** ML ***
    1.41 -
    1.42 + 
    1.43  * Rules and tactics that read instantiations (read_instantiate,
    1.44  res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
    1.45  context, which is required for parsing and type-checking.  Moreover,