diff options
| author | Gerwin Klein | 2003-12-23 12:24:06 +0000 |
|---|---|---|
| committer | Gerwin Klein | 2003-12-23 12:24:06 +0000 |
| commit | 43223f0fd8c99a6f85fbcf206e34aef7b8ffe47c (patch) | |
| tree | a1fcde78885fe70d71a346354389ace90514c353 | |
| parent | d12f805c9eb596abfb58fb963e99e853c23d8a7f (diff) | |
removed bold, no longer supported by x-symbol
| -rw-r--r-- | isa/Example-Xsym.ML | 2 | ||||
| -rw-r--r-- | isar/isar.el | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/isa/Example-Xsym.ML b/isa/Example-Xsym.ML index c9d40747..ed97c291 100644 --- a/isa/Example-Xsym.ML +++ b/isa/Example-Xsym.ML @@ -5,7 +5,7 @@ Just a version of Example.ML using XSymbol. - Also subscripts/superscripts/bold: A\<^sup>1 \\<or> A\<^sub>2 \\<or> A\<^bold>3 + Also subscripts/superscripts: A\<^sup>1 \\<or> A\<^sub>2 [NB: these can't be used in identifiers or otherwise parsed by Isabelle unless declared as part of a theory's concrete syntax, see docs or examples in HOL/IMP.] diff --git a/isar/isar.el b/isar/isar.el index 5a7831f7..5b4c0b97 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -495,7 +495,6 @@ proof-shell-retract-files-regexp." ;; Commands specific to isar ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(proof-defshortcut isar-bold "\\<^bold>" [(control b)]) (proof-defshortcut isar-super "\\<^sup>" [(control u)]) (proof-defshortcut isar-sub "\\<^sub>" [(control l)]) |