diff options
| author | Makarius Wenzel | 2010-08-03 15:29:35 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2010-08-03 15:29:35 +0000 |
| commit | d17c13bee1a8cf938c8c1357fd152e1d71c8e4c7 (patch) | |
| tree | 55411fa3179cab2e1defe5b034fc8560735cbfa5 /generic | |
| 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 'generic')
0 files changed, 0 insertions, 0 deletions