--- a/src/FOLP/ex/foundn.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/foundn.ML Fri Oct 10 16:29:41 1997 +0200
@@ -99,7 +99,7 @@
(*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u.ALL x.EX v.ALL y.EX w. P(u,x,v,y,w)";
+goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
@@ -108,7 +108,7 @@
val prems =
-goal IFOLP.thy "p : (EX z.F(z)) & B ==> ?p:(EX z. F(z) & B)";
+goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);