# Default interpretation of some Isabelle symbols \ code: 0x01d7ec \ code: 0x01d7ed \ code: 0x01d7ee \ code: 0x01d7ef \ code: 0x01d7f0 \ code: 0x01d7f1 \ code: 0x01d7f2 \ code: 0x01d7f3 \ code: 0x01d7f4 \ code: 0x01d7f5 \ code: 0x01d49c \ code: 0x00212c \ code: 0x01d49e \ code: 0x01d49f \ code: 0x002130 \ code: 0x002131 \ code: 0x01d4a2 \ code: 0x00210b \ code: 0x002110 \ code: 0x01d4a5 \ code: 0x01d4a6 \ code: 0x002112 \ code: 0x002133 \ code: 0x01d4a9 \ code: 0x01d4aa \

code: 0x01d5c9 \ code: 0x01d5ca \ code: 0x01d5cb \ code: 0x01d5cc \ code: 0x01d5cd \ code: 0x01d5ce \ code: 0x01d5cf \ code: 0x01d5d0 \ code: 0x01d5d1 \ code: 0x01d5d2 \ code: 0x01d5d3 \ code: 0x01d504 \ code: 0x01d505 \ code: 0x00212d \

code: 0x01d507 \ code: 0x01d508 \ code: 0x01d509 \ code: 0x01d50a \ code: 0x00210c #\ code: 0x01d50c \ code: 0x01d50d \ code: 0x01d50e \ code: 0x01d50f \ code: 0x01d510 \ code: 0x01d511 \ code: 0x01d512 \ code: 0x01d513 \ code: 0x01d514 #\ code: 0x01d515 \ code: 0x01d516 \ code: 0x01d517 \ code: 0x01d518 \ code: 0x01d519 \ code: 0x01d51a \ code: 0x01d51b \ code: 0x01d51c \ code: 0x002128 \ code: 0x01d51e \ code: 0x01d51f \ code: 0x01d520 \
code: 0x01d521 \ code: 0x01d522 \ code: 0x01d523 \ code: 0x01d524 \ code: 0x01d525 \ code: 0x01d526 \ code: 0x01d527 \ code: 0x01d528 \ code: 0x01d529 \ code: 0x01d52a \ code: 0x01d52b \ code: 0x01d52c \ code: 0x01d52d \ code: 0x01d52e \ code: 0x01d52f \ code: 0x01d530 \ code: 0x01d531 \ code: 0x01d532 \ code: 0x01d533 \ code: 0x01d534 \ code: 0x01d535 \ code: 0x01d536 \ code: 0x01d537 \ code: 0x0003b1 \ code: 0x0003b2 \ code: 0x0003b3 \ code: 0x0003b4 \ code: 0x0003b5 \ code: 0x0003b6 \ code: 0x0003b7 \ code: 0x0003b8 \ code: 0x0003b9 \ code: 0x0003ba \ code: 0x0003bb abbrev: % \ code: 0x0003bc \ code: 0x0003bd \ code: 0x0003be \ code: 0x0003c0 \ code: 0x0003c1 \ code: 0x0003c3 \ code: 0x0003c4 \ code: 0x0003c5 \ code: 0x0003c6 \ code: 0x0003c7 \ code: 0x0003c8 \ code: 0x0003c9 \ code: 0x000393 \ code: 0x000394 \ code: 0x000398 \ code: 0x00039b \ code: 0x00039e \ code: 0x0003a0 \ code: 0x0003a3 \ code: 0x0003a5 \ code: 0x0003a6 \ code: 0x0003a8 \ code: 0x0003a9 \ code: 0x01d539 \ code: 0x002102 \ code: 0x002115 \ code: 0x00211a \ code: 0x00211d \ code: 0x002124 \ code: 0x002190 \ code: 0x0027f5 \ code: 0x002192 abbrev: -> \ code: 0x0027f6 abbrev: --> \ code: 0x0021d0 \ code: 0x0027f8 \ code: 0x0021d2 abbrev: => \ code: 0x0027f9 abbrev: ==> \ code: 0x002194 \ code: 0x0027f7 abbrev: <-> \ code: 0x0021d4 \ code: 0x0027fa abbrev: <=> \ code: 0x0021a6 abbrev: |-> \ code: 0x0027fc abbrev: |--> \ code: 0x002500 \ code: 0x002550 \ code: 0x0021a9 \ code: 0x0021aa \ code: 0x0021bd \ code: 0x0021c1 \ code: 0x0021bc \ code: 0x0021c0 \ code: 0x0021cc \ code: 0x00219d abbrev: ~> \ code: 0x0021c3 \ code: 0x0021c2 \ code: 0x0021bf #\ code: 0x0021be \ code: 0x0021be \ code: 0x002237 \ code: 0x002191 \ code: 0x0021d1 \ code: 0x002193 \ code: 0x0021d3 \ code: 0x002195 \ code: 0x0021d5 \ code: 0x0027e8 abbrev: <. \ code: 0x0027e9 abbrev: .> \ code: 0x002308 \ code: 0x002309 \ code: 0x00230a \ code: 0x00230b \ code: 0x002987 abbrev: (| \ code: 0x002988 abbrev: |) \ code: 0x0027e6 abbrev: [| \ code: 0x0027e7 abbrev: |] \ code: 0x002983 abbrev: {. \ code: 0x002984 abbrev: .} \ code: 0x0000ab abbrev: << \ code: 0x0000bb abbrev: >> \ code: 0x0022a5 \ code: 0x0022a4 \ code: 0x002227 abbrev: /\ \ code: 0x0022c0 abbrev: !! \ code: 0x002228 abbrev: \/ \ code: 0x0022c1 abbrev: ?? \ code: 0x002200 abbrev: ! \ code: 0x002203 abbrev: ? \ code: 0x002204 abbrev: ~? \ code: 0x0000ac abbrev: ~ \ code: 0x0025a1 \ code: 0x0025c7 \ code: 0x0022a2 abbrev: |- \ code: 0x0022a8 abbrev: |= \ code: 0x0022a9 abbrev: ||- \ code: 0x0022ab abbrev: ||= \ code: 0x0022a3 abbrev: -| \ code: 0x00221a \ code: 0x002264 abbrev: <= \ code: 0x002265 abbrev: >= \ code: 0x00226a \ code: 0x00226b \ code: 0x002272 \ code: 0x002273 \ code: 0x002a85 \ code: 0x002a86 \ code: 0x002208 abbrev: : \ code: 0x002209 abbrev: ~: \ code: 0x002282 \ code: 0x002283 \ code: 0x002286 abbrev: (= \ code: 0x002287 abbrev: =) \ code: 0x00228f \ code: 0x002290 \ code: 0x002291 abbrev: [= \ code: 0x002292 abbrev: =] \ code: 0x002229 abbrev: Int \ code: 0x0022c2 abbrev: Inter \ code: 0x00222a abbrev: Un \ code: 0x0022c3 abbrev: Union \ code: 0x002294 \ code: 0x002a06 \ code: 0x002293 \ code: 0x002a05 \ code: 0x002216 \ code: 0x00221d \ code: 0x00228e \ code: 0x002a04 \ code: 0x002260 abbrev: ~= \ code: 0x00223c \ code: 0x002250 \ code: 0x002243 \ code: 0x002248 \ code: 0x00224d \ code: 0x002245 \ code: 0x002323 \ code: 0x002261 abbrev: == \ code: 0x002322 \ code: 0x0022c8 \ code: 0x002a1d \ code: 0x00227a \ code: 0x00227b \ code: 0x00227c \ code: 0x00227d \ code: 0x002225 abbrev: || \ code: 0x0000a6 \ code: 0x0000b1 \ code: 0x002213 \ code: 0x0000d7 \
code: 0x0000f7 \ code: 0x0022c5 \ code: 0x0022c6 \ code: 0x002219 \ code: 0x002218 \ code: 0x002020 \ code: 0x002021 \ code: 0x0022b2 \ code: 0x0022b3 \ code: 0x0022b4 \ code: 0x0022b5 \ code: 0x0025c3 \ code: 0x0025b9 \ code: 0x0025b3 \ code: 0x00225c \ code: 0x002295 abbrev: +o \ code: 0x002a01 abbrev: +O \ code: 0x002297 abbrev: *o \ code: 0x002a02 abbrev: *O \ code: 0x002299 abbrev: .o \ code: 0x002a00 abbrev: .O \ code: 0x002296 abbrev: -o \ code: 0x002298 abbrev: /o \ code: 0x002026 abbrev: ... \ code: 0x0022ef \ code: 0x002211 abbrev: SUM \ code: 0x00220f abbrev: PROD \ code: 0x002210 \ code: 0x00221e \ code: 0x00222b \ code: 0x00222e \ code: 0x002663 \ code: 0x002662 \ code: 0x002661 \ code: 0x002660 \ code: 0x002135 \ code: 0x002205 \ code: 0x002207 \ code: 0x002202 \ code: 0x00211c \ code: 0x002111 \ code: 0x00266d \ code: 0x00266e \ code: 0x00266f \ code: 0x002220 \ code: 0x0000a9 \ code: 0x0000ae \ code: 0x0000ad \ code: 0x0000af \ code: 0x0000b9 \ code: 0x0000bc \ code: 0x0000b2 \ code: 0x0000bd \ code: 0x0000b3 \ code: 0x0000be \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 \ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac \ code: 0x0000a3 \ code: 0x0000a5 \ code: 0x0000a2 \ code: 0x0000a4 \ code: 0x0000b0 \ code: 0x002a3f \ code: 0x002127 \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 \ code: 0x0022c4 \ code: 0x0000b4 \ code: 0x000131 \ code: 0x0000a8 \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x0003f5 \<^sub> code: 0x0021e9 abbrev: =_ \<^sup> code: 0x0021e7 abbrev: =^ \<^isub> code: 0x0021e3 abbrev: -_ \<^isup> code: 0x0021e1 abbrev: -^ \<^bsub> code: 0x0021d8 abbrev: =_( \<^esub> code: 0x0021d9 abbrev: =_) \<^bsup> code: 0x0021d7 abbrev: =^( \<^esup> code: 0x0021d6 abbrev: =^) \<^bold> code: 0x002759 abbrev: -.

code: 0x01d4ab \ code: 0x01d4ac \ code: 0x00211b \ code: 0x01d4ae \ code: 0x01d4af \ code: 0x01d4b0 \ code: 0x01d4b1 \ code: 0x01d4b2 \ code: 0x01d4b3 \ code: 0x01d4b4 \ code: 0x01d4b5 \ code: 0x01d5ba \ code: 0x01d5bb \ code: 0x01d5bc \ code: 0x01d5bd \ code: 0x01d5be \ code: 0x01d5bf \ code: 0x01d5c0 \ code: 0x01d5c1 \ code: 0x01d5c2 \ code: 0x01d5c3 \ code: 0x01d5c4 \ code: 0x01d5c5 \ code: 0x01d5c6 \ code: 0x01d5c7 \ code: 0x01d5c8 \