--- a/src/HOL/Induct/Sexp.thy Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.thy Wed Aug 08 14:51:10 2001 +0200
@@ -28,9 +28,9 @@
defs
sexp_case_def
- "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))
- | (? k. M=Numb(k) & z=d(k))
- | (? N1 N2. M = Scons N1 N2 & z=e N1 N2)"
+ "sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x))
+ | (EX k. M=Numb(k) & z=d(k))
+ | (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)"
pred_sexp_def
"pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"