# HG changeset patch
# User paulson
# Date 990449591 -7200
# Node ID 6a20952757b29b0b8512799273ae0c1629598d7a
# Parent  01cbbf33779b5f4a938b637d5eadbe533e19f17e
fixed the X-symbol syntax for lambda

diff -r 01cbbf33779b -r 6a20952757b2 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Mon May 21 14:52:27 2001 +0200
+++ b/src/ZF/ZF.thy	Mon May 21 14:53:11 2001 +0200
@@ -157,7 +157,7 @@
   "@UNION"    :: [pttrn, i, i] => i        ("(3\\<Union>_\\<in>_./ _)" 10)
   "@PROD"     :: [pttrn, i, i] => i        ("(3\\<Pi>_\\<in>_./ _)" 10)
   "@SUM"      :: [pttrn, i, i] => i        ("(3\\<Sigma>_\\<in>_./ _)" 10)
-  "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_:_./ _)" 10)
+  "@lam"      :: [pttrn, i, i] => i        ("(3\\<lambda>_\\<in>_./ _)" 10)
   "@Ball"     :: [pttrn, i, o] => o        ("(3\\<forall>_\\<in>_./ _)" 10)
   "@Bex"      :: [pttrn, i, o] => o        ("(3\\<exists>_\\<in>_./ _)" 10)