| changeset 3835 | 9a5a4e123859 |
| parent 2469 | b50b8c0eec01 |
| child 5204 | 858da18069d7 |
--- a/src/FOL/ex/intro.ML Fri Oct 10 15:51:38 1997 +0200 +++ b/src/FOL/ex/intro.ML Fri Oct 10 15:52:12 1997 +0200 @@ -32,7 +32,7 @@ result(); (*Correct version, delaying use of "spec" until last*) -goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; +goal FOL.thy "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"; by (rtac impI 1); by (rtac allI 1); by (rtac allI 1);