diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-05-06 18:33:53 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-05-06 18:33:53 +0000 |
| commit | 969d971f2d7339a3a03271eb86e82452599348a0 (patch) | |
| tree | e62886a2ef8327868da32e953fd549c756cee7cb | |
| parent | 8e565189e1f86154e34483c02011a4268a5b1814 (diff) | |
Patch from Brother Makarius
| -rw-r--r-- | isa/x-symbol-isabelle.el | 1 | ||||
| -rw-r--r-- | 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)]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |