From 3c69e788f89e0db0600cc354c7893dd8129ed3a8 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Thu, 30 Aug 2001 19:26:34 +0000
Subject: added proof-script-integral-proofs ("Whether the complete text after
 a   goal confines the actual proof.");

---
 generic/proof-config.el | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/generic/proof-config.el b/generic/proof-config.el
index e65f1722..419953fa 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -799,6 +799,22 @@ the parsing functions went through several iterations and the final
   :type 'boolean
   :group 'prover-config)
 
+
+(defcustom proof-script-integral-proofs nil
+  "Whether the complete text after a goal confines the actual proof.
+
+In structured proof languages like Isabelle/Isar a theorem is
+established by a goal statement (with full information about the
+result, including name and statement), followed by a self-contained
+piece of text for the proof.  The latter should be treated as an
+integral entity for purposes of hiding proof bodies etc.
+
+This variable is better set to nil for tactical provers (like Coq)
+where important information about the result is spread over the
+initial ``goal'' and the final ``save'' command."
+  :type 'boolean
+  :group 'prover-config)
+
 ;; Unadvertised customization variable
 (defvar proof-script-fly-past-comments t
   "*If non-nil, fly past comments when scripting, coalescing them into single spans.")
-- 
cgit v1.2.3