diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2010-08-03 15:29:35 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2010-08-03 15:29:35 +0000 |
| commit | d17c13bee1a8cf938c8c1357fd152e1d71c8e4c7 (patch) | |
| tree | 55411fa3179cab2e1defe5b034fc8560735cbfa5 /isar | |
| parent | ec4179d75c368d1a0ef10deabcdce23ca0ac490e (diff) | |
less surprising unicode tokens: <-> corresponds to longleftrightarrow in common Isabelle theories (according to symbol length not shape), emdash is not predefined by default and confuses typical LaTeX source;
Diffstat (limited to 'isar')
| -rw-r--r-- | isar/isar-unicode-tokens.el | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index 581543ab..ce1620a6 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -593,7 +593,7 @@ For Isabelle, the token TOKNAME is made into the token \\< TNAME >." ("==>" . "\\<Longrightarrow>") ("<==>" . "\\<Longleftrightarrow>") ("|-->" . "\\<longmapsto>") - ("<-->" . "\\<longleftrightarrow>") + ("<->" . "\\<longleftrightarrow>") ("<<" . "\\<guillemotleft>") (">>" . "\\<guillemotright>") ("<>" . "\\<diamond>") @@ -601,7 +601,6 @@ For Isabelle, the token TOKNAME is made into the token \\< TNAME >." ("|]" . "\\<rbrakk>") ("{|" . "\\<lbrace>") ("|}" . "\\<rbrace>") - ("---" . "\\<emdash>") ("(|" . "\\<lparr>") ("|)" . "\\<rparr>") ;; useful for unicode-tokens-replace-shortcuts |