aboutsummaryrefslogtreecommitdiff
path: root/isa
diff options
context:
space:
mode:
authorMakarius Wenzel2005-09-01 14:18:10 +0000
committerMakarius Wenzel2005-09-01 14:18:10 +0000
commit73375b71d50c9be41127d424b4868a5d0ccdba80 (patch)
tree0f8904db9c051169d2ab4b250b6cc87ec2380d4e /isa
parent2b2dab487ffa46b7ddaf930071a0e6fa70b1bbc9 (diff)
tuned ML code for manipulating print_mode;
Diffstat (limited to 'isa')
-rw-r--r--isa/x-symbol-isa.el4
1 files changed, 2 insertions, 2 deletions
diff --git a/isa/x-symbol-isa.el b/isa/x-symbol-isa.el
index d1ff4cb7..71dcb41e 100644
--- a/isa/x-symbol-isa.el
+++ b/isa/x-symbol-isa.el
@@ -12,9 +12,9 @@
(setq proof-xsym-extra-modes '(thy-mode)
proof-xsym-activate-command
- "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);"
+ "change print_mode (insert (op =) \"xsymbols\")"
proof-xsym-deactivate-command
- "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);")
+ "change print_mode (remove (op =) \"xsymbols\")")