2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> |
3 <html xmlns="http://www.w3.org/1999/xhtml"> |
3 <html xmlns="http://www.w3.org/1999/xhtml"> |
4 |
4 |
5 <head> |
5 <head> |
6 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> |
6 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> |
|
7 <style type="text/css" media="screen"> |
|
8 body { font-family: IsabelleText; font-size: 14pt; } |
|
9 </style> |
7 <title>Notes on the Isabelle/jEdit Prover IDE</title> |
10 <title>Notes on the Isabelle/jEdit Prover IDE</title> |
8 </head> |
11 </head> |
9 |
12 |
10 <body> |
13 <body> |
11 |
14 |
45 ≤, ≥, ⊓, ⊔, …<br/> |
48 ≤, ≥, ⊓, ⊔, …<br/> |
46 ℵ, △, ∇, …<br/> |
49 ℵ, △, ∇, …<br/> |
47 <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/> |
50 <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/> |
48 </li> |
51 </li> |
49 |
52 |
|
53 <li>There are some special control symbols to modify the style of a |
|
54 <em>single</em> symbol:<br/> |
|
55 ⇩ subscript<br/> |
|
56 ⇧ superscript<br/> |
|
57 ⇣ subscript within identifier<br/> |
|
58 ⇡ superscript within identifier<br/> |
|
59 ❙ bold face</li> |
|
60 |
50 <li>A default mapping relates some Isabelle symbols to Unicode points |
61 <li>A default mapping relates some Isabelle symbols to Unicode points |
51 (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>). |
62 (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>). |
52 </li> |
63 </li> |
53 |
64 |
54 <li>The <em>IsabelleText</em> font ensures that Unicode points are actually |
65 <li>The <em>IsabelleText</em> font ensures that Unicode points are actually |
78 <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr> |
89 <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr> |
79 <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr> |
90 <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr> |
80 <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr> |
91 <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr> |
81 <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr> |
92 <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr> |
82 <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr> |
93 <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr> |
|
94 |
|
95 <tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr> |
|
96 <tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr> |
|
97 <tr><td>isup</td> <td><tt>-_</tt></td> <td>⇣</td></tr> |
|
98 <tr><td>isub</td> <td><tt>-^</tt></td> <td>⇡</td></tr> |
|
99 <tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr> |
|
100 |
83 </table> |
101 </table> |
84 </li> |
102 </li> |
85 </ul> |
103 </ul> |
86 </li> |
104 </li> |
87 |
105 |