From d53e2c48e6cf6284a4d87010efe41eac457b2b1f Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Sun, 4 Jun 2000 12:40:18 +0000
Subject: replaced isa-verbatim by isabelle-verbatim;

---
 isa/isa-syntax.el | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 87f8dfaf..f83e0e5c 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -181,13 +181,6 @@
   (proof-ids-to-regexp isa-keywords-proof-commands)
   "Regexp to match proof commands, with no extra output (apart from proof state)")
 
-(defconst isa-verbatim-regexp "^\^VERBATIM: \\(.*\\)"
-  "Regexp matching internal marker for verbatim command output")
-
-(defun isa-verbatim (str)
-  "Mark internal command for verbatim output"
-  (concat "\^VERBATIM: " str))
-
 
 ;; ----- Isabelle inner syntax hilite
 
-- 
cgit v1.2.3