diff -r 250e9be7a09d -r cb559bd0b03c src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Oct 11 10:51:19 2004 +0200
+++ b/src/Pure/proof_general.ML	Mon Oct 11 10:52:18 2004 +0200
@@ -600,7 +600,10 @@
        proof_option)),
      ("theorem-dependencies", 
        ("Track theorem dependencies within Proof General",
-	thm_deps_option))])
+	thm_deps_option)),
+     ("skip-proofs", 
+      ("Skip all proof scripts (interactive-only)",
+       bool_option Toplevel.skip_proofs))])
    ];
 end