# HG changeset patch
# User wenzelm
# Date 1308516795 -7200
# Node ID 3d42dea16357ce89c7f8c2aba09343428210515b
# Parent 882108e9536a6c0e906cf0d1916d7bbfcc599bc7
explain special control symbols;
diff -r 882108e9536a -r 3d42dea16357 src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html Sun Jun 19 22:52:49 2011 +0200
+++ b/src/Tools/jEdit/README.html Sun Jun 19 22:53:15 2011 +0200
@@ -4,6 +4,9 @@
+
Notes on the Isabelle/jEdit Prover IDE
@@ -47,6 +50,14 @@
\<foo>, \<bar>, \<baz>, …
+ There are some special control symbols to modify the style of a
+ single symbol:
+ ⇩ subscript
+ ⇧ superscript
+ ⇣ subscript within identifier
+ ⇡ superscript within identifier
+ ❙ bold face
+
A default mapping relates some Isabelle symbols to Unicode points
(see $ISABELLE_HOME/etc/symbols and $ISABELLE_HOME_USER/etc/symbols).
@@ -80,6 +91,13 @@
| noteq | ~= | ≠ |
| in | : | ∈ |
| notin | ~: | ∉ |
+
+ | sub | =_ | ⇩ |
+ | sup | =^ | ⇧ |
+ | isup | -_ | ⇣ |
+ | isub | -^ | ⇡ |
+ | bold | -. | ❙ |
+