src/Pure/proof_general.ML
changeset 15238 cb559bd0b03c
parent 15225 68ab0f4eb457
child 15253 6e20cc79bde6
--- 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