# HG changeset patch # User paulson # Date 864644025 -7200 # Node ID 4e7dfe8ae41baa4fbcc7c9c2cef828a9743adeaf # Parent 5101517c26141bae051e3dafc16384c0c6f286eb Added a missing "result();" after problem 43. diff -r 5101517c2614 -r 4e7dfe8ae41b src/HOL/ex/cla.ML --- 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) --> \