--- a/src/HOL/Induct/SList.thy Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/SList.thy Wed Aug 08 14:51:10 2001 +0200
@@ -10,7 +10,7 @@
so that list can serve as a "functor" for defining other recursive types
*)
-SList = Sexp +
+SList = Sexp + Hilbert_Choice (*gives us "inv"*) +
consts
--- a/src/HOL/Induct/Sexp.ML Wed Aug 08 14:50:28 2001 +0200
+++ b/src/HOL/Induct/Sexp.ML Wed Aug 08 14:51:10 2001 +0200
@@ -6,8 +6,6 @@
S-expressions, general binary trees for defining recursive data structures
*)
-open Sexp;
-
(** sexp_case **)
Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
--- 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)}"