Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added a missing "result();" after problem 43.
authorpaulson
Mon, 26 May 1997 12:53:45 +0200
changeset 3347 4e7dfe8ae41b
parent 3346 5101517c2614
child 3348 3f9a806f061e
Added a missing "result();" after problem 43.
src/HOL/ex/cla.ML file | annotate | diff | comparison | revisions 
--- 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) -->                                    \
isabelle