src/HOL/Hilbert_Choice.thy
changeset 13764 3e180bf68496
parent 13763 f94b569cd610
child 14115 65ec3f73d00b
--- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 15:02:40 2002 +0100
@@ -22,7 +22,7 @@
 syntax
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
 translations
-  "SOME x. P" => "Eps (%x. P)"
+  "SOME x. P" == "Eps (%x. P)"
 
 print_translation {*
 (* to avoid eta-contraction of body *)