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

code: 0x01d507 font: Isabelle -\ code: 0x01d508 font: Isabelle -\ code: 0x01d509 font: Isabelle -\ code: 0x01d50a font: Isabelle -\ code: 0x00210c font: Isabelle -#\ code: 0x01d50c font: Isabelle -\ code: 0x01d50d font: Isabelle -\ code: 0x01d50e font: Isabelle -\ code: 0x01d50f font: Isabelle -\ code: 0x01d510 font: Isabelle -\ code: 0x01d511 font: Isabelle -\ code: 0x01d512 font: Isabelle -\ code: 0x01d513 font: Isabelle -\ code: 0x01d514 font: Isabelle -#\ code: 0x01d515 font: Isabelle -\ code: 0x01d516 font: Isabelle -\code: 0x01d517 font: Isabelle -\ code: 0x01d518 font: Isabelle -\ code: 0x01d519 font: Isabelle -\ code: 0x01d51a font: Isabelle -\ code: 0x01d51b font: Isabelle -\ code: 0x01d51c font: Isabelle -\ code: 0x002128 font: Isabelle -\ code: 0x01d51e font: Isabelle -\ code: 0x01d51f font: Isabelle -\ code: 0x01d520 font: Isabelle -\

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