src/FOLP/ex/foundn.ML
changeset 3836 f1a1817659e6
parent 1464 a608f83e3421
child 17480 fd19f77dcf60
--- 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);