diff options
| author | Makarius Wenzel | 1999-05-25 08:14:38 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-05-25 08:14:38 +0000 |
| commit | c306e994165b94c497e7de678d80b6b84fe549cb (patch) | |
| tree | 6cf2f4db44b6acb5a55392e044ed461a82a5ae52 | |
| parent | cab99ec2d9ea48a99ae1398023b3586e8849cf67 (diff) | |
added proof-really-save-command-p to support
more general qed schemes, such as Isabelle/Isar's nested proofs;
| -rw-r--r-- | generic/proof-config.el | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 6e8c3806..bf898fc4 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -576,6 +576,13 @@ beginning of the entity's region." :type 'function :group 'proof-script) +;; FIXME mmw: increasing the horror even more ... + +(defcustom proof-really-save-command-p (lambda (span cmd) t) + "Is this really a save command?" + :type 'function + :group 'proof-script) + (defcustom proof-lift-global nil "This function lifts local lemmas from inside goals out to top level. This function takes the local goalsave span as an argument. Set this |