NEWS
changeset 14878 b884a7ba7238
parent 14854 61bdf2ae4dc5
child 14885 0a840138dcd7
equal deleted inserted replaced
14877:28084696907f 14878:b884a7ba7238
    68   linear in the number of extensions and not in the number of fields.
    68   linear in the number of extensions and not in the number of fields.
    69   The top-level (users) view on records is preserved.  Potential
    69   The top-level (users) view on records is preserved.  Potential
    70   INCOMPATIBILITY only in strange cases, where the theory depends on
    70   INCOMPATIBILITY only in strange cases, where the theory depends on
    71   the old record representation. The type generated for a record is
    71   the old record representation. The type generated for a record is
    72   called <record_name>_ext_type.
    72   called <record_name>_ext_type.
       
    73 
       
    74 * HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
       
    75 
       
    76   syntax (epsilon)
       
    77     "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
       
    78 
       
    79   The symbol \<some> is displayed as the alternative epsilon of LaTeX
       
    80   and x-symbol; use option '-m epsilon' to get it actually printed.
       
    81   Moreover, the mathematically important symbolic identifier
       
    82   \<epsilon> becomes available as variable, constant etc.
    73 
    83 
    74 * Simplifier: "record_upd_simproc" for simplification of multiple
    84 * Simplifier: "record_upd_simproc" for simplification of multiple
    75   record updates enabled by default.  INCOMPATIBILITY: old proofs
    85   record updates enabled by default.  INCOMPATIBILITY: old proofs
    76   break occasionally, since simplification is more powerful by
    86   break occasionally, since simplification is more powerful by
    77   default.
    87   default.