src/HOL/ex/cla.ML
changeset 3347 4e7dfe8ae41b
parent 3019 ca5a7bbbee6c
child 3842 b55686a7b22c
--- a/src/HOL/ex/cla.ML	Mon May 26 12:44:04 1997 +0200
+++ b/src/HOL/ex/cla.ML	Mon May 26 12:53:45 1997 +0200
@@ -347,7 +347,7 @@
     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
 \ --> (! x. (! y. q x y = (q y x::bool)))";
 by (Blast_tac 1);
-
+result();
 
 writeln"Problem 44";
 goal HOL.thy "(! x. f(x) -->                                    \