equal
deleted
inserted
replaced
186 \<leadsto> code: 0x00219d group: arrow abbrev: .> abbrev: ~> |
186 \<leadsto> code: 0x00219d group: arrow abbrev: .> abbrev: ~> |
187 \<downharpoonleft> code: 0x0021c3 group: arrow |
187 \<downharpoonleft> code: 0x0021c3 group: arrow |
188 \<downharpoonright> code: 0x0021c2 group: arrow |
188 \<downharpoonright> code: 0x0021c2 group: arrow |
189 \<upharpoonleft> code: 0x0021bf group: arrow |
189 \<upharpoonleft> code: 0x0021bf group: arrow |
190 #\<upharpoonright> code: 0x0021be group: arrow |
190 #\<upharpoonright> code: 0x0021be group: arrow |
191 \<restriction> code: 0x0021be group: punctuation |
191 \<restriction> code: 0x0021be group: operator |
192 \<Colon> code: 0x002237 group: punctuation |
192 \<Colon> code: 0x002237 group: punctuation |
193 \<up> code: 0x002191 group: arrow |
193 \<up> code: 0x002191 group: arrow |
194 \<Up> code: 0x0021d1 group: arrow |
194 \<Up> code: 0x0021d1 group: arrow |
195 \<down> code: 0x002193 group: arrow |
195 \<down> code: 0x002193 group: arrow |
196 \<Down> code: 0x0021d3 group: arrow |
196 \<Down> code: 0x0021d3 group: arrow |
325 \<sharp> code: 0x00266f |
325 \<sharp> code: 0x00266f |
326 \<angle> code: 0x002220 |
326 \<angle> code: 0x002220 |
327 \<copyright> code: 0x0000a9 |
327 \<copyright> code: 0x0000a9 |
328 \<registered> code: 0x0000ae |
328 \<registered> code: 0x0000ae |
329 \<hyphen> code: 0x002010 group: punctuation |
329 \<hyphen> code: 0x002010 group: punctuation |
330 \<inverse> code: 0x0000af group: punctuation |
330 \<inverse> code: 0x0000af group: operator |
331 \<onequarter> code: 0x0000bc group: digit |
331 \<onequarter> code: 0x0000bc group: digit |
332 \<onehalf> code: 0x0000bd group: digit |
332 \<onehalf> code: 0x0000bd group: digit |
333 \<threequarters> code: 0x0000be group: digit |
333 \<threequarters> code: 0x0000be group: digit |
334 \<ordfeminine> code: 0x0000aa |
334 \<ordfeminine> code: 0x0000aa |
335 \<ordmasculine> code: 0x0000ba |
335 \<ordmasculine> code: 0x0000ba |
351 \<acute> code: 0x0000b4 |
351 \<acute> code: 0x0000b4 |
352 \<index> code: 0x000131 |
352 \<index> code: 0x000131 |
353 \<dieresis> code: 0x0000a8 |
353 \<dieresis> code: 0x0000a8 |
354 \<cedilla> code: 0x0000b8 |
354 \<cedilla> code: 0x0000b8 |
355 \<hungarumlaut> code: 0x0002dd |
355 \<hungarumlaut> code: 0x0002dd |
356 \<bind> code: 0x00291c abbrev: >>= |
356 \<bind> code: 0x00291c group: operator abbrev: >>= |
357 \<then> code: 0x002aa2 abbrev: >> |
357 \<then> code: 0x002aa2 group: operator abbrev: >> |
358 \<some> code: 0x0003f5 |
358 \<some> code: 0x0003f5 |
359 \<hole> code: 0x002311 |
359 \<hole> code: 0x002311 |
360 \<newline> code: 0x0023ce |
360 \<newline> code: 0x0023ce |
361 \<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono |
361 \<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono |
362 \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono |
362 \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono |