From 969d971f2d7339a3a03271eb86e82452599348a0 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 6 May 2004 18:33:53 +0000
Subject: Patch from Brother Makarius

---
 isa/x-symbol-isabelle.el |  1 +
 isar/isar.el             | 13 +++++++------
 2 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index 1bed377e..f4ee80dd 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -243,6 +243,7 @@ See `x-symbol-language-access-alist' for details."
     (logicalor "\\<or>")
     (universal1 "\\<forall>")
     (existential1 "\\<exists>")
+    (epsilon "\\<some>")
     (biglogicaland "\\<And>")
     (ceilingleft "\\<lceil>")
     (ceilingright "\\<rceil>")
diff --git a/isar/isar.el b/isar/isar.el
index 740b327d..e4506266 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -505,12 +505,13 @@ proof-shell-retract-files-regexp."
 ;;   Commands specific to isar                                      ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(proof-defshortcut isar-super    "\\<^sup>" [(control u)])
-(proof-defshortcut isar-sub      "\\<^sub>"   [(control l)])
-(proof-defshortcut isar-longsup  "\\<^bsup>%p\\<^esup>" [u])
-(proof-defshortcut isar-longsub  "\\<^bsub>%p\\<^esub>" [l])
-(proof-defshortcut isar-idsub    "\\<^isub>" [(control i)])
-(proof-defshortcut isar-raw      "\\<^raw:%p>" [(control r)])
+(proof-defshortcut isar-super     "\\<^sup>%p" [(control u)])
+(proof-defshortcut isar-sub       "\\<^sub>%p" [(control l)])
+(proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [u])
+(proof-defshortcut isar-longsub   "\\<^bsub>%p\\<^esub>" [l])
+(proof-defshortcut isar-idsub     "\\<^isub>%p" [(control i)])
+(proof-defshortcut isar-raw       "\\<^raw:%p>" [(control r)])
+(proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)])
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-- 
cgit v1.2.3