aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 01:41:55 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-08-29 01:41:55 +0000
commitaca85757bdf148cb4b43ba5a60c7d397215d74d4 (patch)
treee7b609a4ad4bdce42dede700a7f09f28c978fefd /isa
parent4148c1e57a81ea19d4ab8f3f4a271bf08a7dcde3 (diff)
Dependencies classed as experimental.
Diffstat (limited to 'isa')
-rw-r--r--isa/isabelle-system.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 62d7e051..a57d65ca 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -354,11 +354,12 @@ until Proof General is restarted."
:type 'boolean
:setting "Library.timing:=%b;")
+(if proof-experimental-features
(defpacustom theorem-dependencies nil
"Whether to track theorem dependencies within Proof General."
:type 'boolean
:setting ("print_mode := ([\"thm_deps\"] @ ! print_mode);" .
- "print_mode := (Library.gen_rems (op =) (! print_mode, [\"thm_deps\"]));"))
+ "print_mode := (Library.gen_rems (op =) (! print_mode, [\"thm_deps\"]));")))
(defpacustom goals-limit 10
"Setting for maximum number of goals printed in Isabelle."