# HG changeset patch
# User wenzelm
# Date 1086524403 -7200
# Node ID b884a7ba723847754435736b8d4f561175cd3d19
# Parent  28084696907fcb9f304106da23e73db7284d6141
HOL: symbolic syntax of Eps;

diff -r 28084696907f -r b884a7ba7238 NEWS
--- a/NEWS	Sat Jun 05 18:34:06 2004 +0200
+++ b/NEWS	Sun Jun 06 14:20:03 2004 +0200
@@ -71,6 +71,16 @@
   the old record representation. The type generated for a record is
   called <record_name>_ext_type.
 
+* HOL: symbolic syntax of Hilbert Choice Operator is now as follows:
+
+  syntax (epsilon)
+    "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
+
+  The symbol \<some> is displayed as the alternative epsilon of LaTeX
+  and x-symbol; use option '-m epsilon' to get it actually printed.
+  Moreover, the mathematically important symbolic identifier
+  \<epsilon> becomes available as variable, constant etc.
+
 * Simplifier: "record_upd_simproc" for simplification of multiple
   record updates enabled by default.  INCOMPATIBILITY: old proofs
   break occasionally, since simplification is more powerful by