--- a/src/HOL/Main.thy Thu May 31 18:16:52 2007 +0200 +++ b/src/HOL/Main.thy Thu May 31 18:16:54 2007 +0200 @@ -18,4 +18,6 @@ setup ResAxioms.setup +ML {* val HOL_proofs = !proofs *} + end