--- a/src/HOL/Main.thy Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Main.thy Wed Sep 17 21:27:14 2008 +0200
@@ -8,8 +8,6 @@
imports Plain Code_Eval Map Nat_Int_Bij Recdef
begin
-ML {* val HOL_proofs = ! Proofterm.proofs *}
-
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
end