From d0c6365a7cbc9ec76472ce49cdda850b282834fb Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 8 May 2007 15:06:32 +0000
Subject: undo: removed confusing comment;

---
 isar/isar-syntax.el | 6 ------
 1 file changed, 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 ";"))
-- 
cgit v1.2.3