--- a/src/FOLP/ex/intro.ML Fri Oct 10 15:52:12 1997 +0200
+++ b/src/FOLP/ex/intro.ML Fri Oct 10 16:29:41 1997 +0200
@@ -32,7 +32,7 @@
result();
(*Correct version, delaying use of "spec" until last*)
-goal FOLP.thy "?p:(ALL x y.P(x,y)) --> (ALL z w.P(w,z))";
+goal FOLP.thy "?p:(ALL x y. P(x,y)) --> (ALL z w. P(w,z))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac allI 1);
@@ -69,7 +69,7 @@
(** Derivation of negation introduction **)
-val prems = goal FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~P";
+val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
by (rewtac not_def);
by (rtac impI 1);
by (resolve_tac prems 1);