diff options
| -rw-r--r-- | isar/isar-syntax.el | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index b70564c7..51fc72b4 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -452,12 +452,6 @@ matches contents of quotes for quoted identifiers.") ;; ----- variations on undo (defconst isar-undo "ProofGeneral.undo;") ;; no output undo -;(defconst isar-undo "undo;") ;; da: ordinary undo: seems more desirable to use this except - ;; for many composed undos undo;undo;undo; we get output - ;; every time which is a bit inefficient (although not that bad - ;; because the print of the theory is short by default). - ;; TODO for Isabelle2007: add - ;; times argument to undo and supress intermediate output. (defun isar-remove (name) (concat "init_toplevel; kill_thy " name ";")) |