HOL: symbolic syntax of Eps;
authorwenzelm
Sun Jun 06 14:20:03 2004 +0200 (2004-06-06)
changeset 14878b884a7ba7238
parent 14877 28084696907f
child 14879 8989eedf72a1
HOL: symbolic syntax of Eps;
NEWS
     1.1 --- a/NEWS	Sat Jun 05 18:34:06 2004 +0200
     1.2 +++ b/NEWS	Sun Jun 06 14:20:03 2004 +0200
     1.3 @@ -71,6 +71,16 @@
     1.4    the old record representation. The type generated for a record is
     1.5    called <record_name>_ext_type.
     1.6  
     1.7 +* HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
     1.8 +
     1.9 +  syntax (epsilon)
    1.10 +    "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
    1.11 +
    1.12 +  The symbol \<some> is displayed as the alternative epsilon of LaTeX
    1.13 +  and x-symbol; use option '-m epsilon' to get it actually printed.
    1.14 +  Moreover, the mathematically important symbolic identifier
    1.15 +  \<epsilon> becomes available as variable, constant etc.
    1.16 +
    1.17  * Simplifier: "record_upd_simproc" for simplification of multiple
    1.18    record updates enabled by default.  INCOMPATIBILITY: old proofs
    1.19    break occasionally, since simplification is more powerful by