#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# Copyright 2017, Data61
# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
# ABN 41 687 119 230.
#
# This software may be distributed and modified according to the terms of
# the BSD 2-Clause license. Note that NO WARRANTY is provided.
# See "LICENSE_BSD2.txt" for details.
#
# @TAG(DATA61_BSD)
#

# THIS FILE WAS GENERATED BY make_isabelle_symbols.py.

from __future__ import absolute_import, division, print_function, \
    unicode_literals
from camkes.internal.seven import cmp, filter, map, zip

ISABELLE_SYMBOLS = frozenset((
    ('\\<zero>', '𝟬'),
    ('\\<one>', '𝟭'),
    ('\\<two>', '𝟮'),
    ('\\<three>', '𝟯'),
    ('\\<four>', '𝟰'),
    ('\\<five>', '𝟱'),
    ('\\<six>', '𝟲'),
    ('\\<seven>', '𝟳'),
    ('\\<eight>', '𝟴'),
    ('\\<nine>', '𝟵'),
    ('\\<A>', '𝒜'),
    ('\\<B>', 'ℬ'),
    ('\\<C>', '𝒞'),
    ('\\<D>', '𝒟'),
    ('\\<E>', 'ℰ'),
    ('\\<F>', 'ℱ'),
    ('\\<G>', '𝒢'),
    ('\\<H>', 'ℋ'),
    ('\\<I>', 'ℐ'),
    ('\\<J>', '𝒥'),
    ('\\<K>', '𝒦'),
    ('\\<L>', 'ℒ'),
    ('\\<M>', 'ℳ'),
    ('\\<N>', '𝒩'),
    ('\\<O>', '𝒪'),
    ('\\<P>', '𝒫'),
    ('\\<Q>', '𝒬'),
    ('\\<R>', 'ℛ'),
    ('\\<S>', '𝒮'),
    ('\\<T>', '𝒯'),
    ('\\<U>', '𝒰'),
    ('\\<V>', '𝒱'),
    ('\\<W>', '𝒲'),
    ('\\<X>', '𝒳'),
    ('\\<Y>', '𝒴'),
    ('\\<Z>', '𝒵'),
    ('\\<a>', '𝖺'),
    ('\\<b>', '𝖻'),
    ('\\<c>', '𝖼'),
    ('\\<d>', '𝖽'),
    ('\\<e>', '𝖾'),
    ('\\<f>', '𝖿'),
    ('\\<g>', '𝗀'),
    ('\\<h>', '𝗁'),
    ('\\<i>', '𝗂'),
    ('\\<j>', '𝗃'),
    ('\\<k>', '𝗄'),
    ('\\<l>', '𝗅'),
    ('\\<m>', '𝗆'),
    ('\\<n>', '𝗇'),
    ('\\<o>', '𝗈'),
    ('\\<p>', '𝗉'),
    ('\\<q>', '𝗊'),
    ('\\<r>', '𝗋'),
    ('\\<s>', '𝗌'),
    ('\\<t>', '𝗍'),
    ('\\<u>', '𝗎'),
    ('\\<v>', '𝗏'),
    ('\\<w>', '𝗐'),
    ('\\<x>', '𝗑'),
    ('\\<y>', '𝗒'),
    ('\\<z>', '𝗓'),
    ('\\<AA>', '𝔄'),
    ('\\<BB>', '𝔅'),
    ('\\<CC>', 'ℭ'),
    ('\\<DD>', '𝔇'),
    ('\\<EE>', '𝔈'),
    ('\\<FF>', '𝔉'),
    ('\\<GG>', '𝔊'),
    ('\\<HH>', 'ℌ'),
    ('\\<II>', 'ℑ'),
    ('\\<JJ>', '𝔍'),
    ('\\<KK>', '𝔎'),
    ('\\<LL>', '𝔏'),
    ('\\<MM>', '𝔐'),
    ('\\<NN>', '𝔑'),
    ('\\<OO>', '𝔒'),
    ('\\<PP>', '𝔓'),
    ('\\<QQ>', '𝔔'),
    ('\\<RR>', 'ℜ'),
    ('\\<SS>', '𝔖'),
    ('\\<TT>', '𝔗'),
    ('\\<UU>', '𝔘'),
    ('\\<VV>', '𝔙'),
    ('\\<WW>', '𝔚'),
    ('\\<XX>', '𝔛'),
    ('\\<YY>', '𝔜'),
    ('\\<ZZ>', 'ℨ'),
    ('\\<aa>', '𝔞'),
    ('\\<bb>', '𝔟'),
    ('\\<cc>', '𝔠'),
    ('\\<dd>', '𝔡'),
    ('\\<ee>', '𝔢'),
    ('\\<ff>', '𝔣'),
    ('\\<gg>', '𝔤'),
    ('\\<hh>', '𝔥'),
    ('\\<ii>', '𝔦'),
    ('\\<jj>', '𝔧'),
    ('\\<kk>', '𝔨'),
    ('\\<ll>', '𝔩'),
    ('\\<mm>', '𝔪'),
    ('\\<nn>', '𝔫'),
    ('\\<oo>', '𝔬'),
    ('\\<pp>', '𝔭'),
    ('\\<qq>', '𝔮'),
    ('\\<rr>', '𝔯'),
    ('\\<ss>', '𝔰'),
    ('\\<tt>', '𝔱'),
    ('\\<uu>', '𝔲'),
    ('\\<vv>', '𝔳'),
    ('\\<ww>', '𝔴'),
    ('\\<xx>', '𝔵'),
    ('\\<yy>', '𝔶'),
    ('\\<zz>', '𝔷'),
    ('\\<alpha>', 'α'),
    ('\\<beta>', 'β'),
    ('\\<gamma>', 'γ'),
    ('\\<delta>', 'δ'),
    ('\\<epsilon>', 'ε'),
    ('\\<zeta>', 'ζ'),
    ('\\<eta>', 'η'),
    ('\\<theta>', 'θ'),
    ('\\<iota>', 'ι'),
    ('\\<kappa>', 'κ'),
    ('\\<lambda>', 'λ'),
    ('\\<mu>', 'μ'),
    ('\\<nu>', 'ν'),
    ('\\<xi>', 'ξ'),
    ('\\<pi>', 'π'),
    ('\\<rho>', 'ρ'),
    ('\\<sigma>', 'σ'),
    ('\\<tau>', 'τ'),
    ('\\<upsilon>', 'υ'),
    ('\\<phi>', 'φ'),
    ('\\<chi>', 'χ'),
    ('\\<psi>', 'ψ'),
    ('\\<omega>', 'ω'),
    ('\\<Gamma>', 'Γ'),
    ('\\<Delta>', 'Δ'),
    ('\\<Theta>', 'Θ'),
    ('\\<Lambda>', 'Λ'),
    ('\\<Xi>', 'Ξ'),
    ('\\<Pi>', 'Π'),
    ('\\<Sigma>', 'Σ'),
    ('\\<Upsilon>', 'Υ'),
    ('\\<Phi>', 'Φ'),
    ('\\<Psi>', 'Ψ'),
    ('\\<Omega>', 'Ω'),
    ('\\<bool>', '𝔹'),
    ('\\<complex>', 'ℂ'),
    ('\\<nat>', 'ℕ'),
    ('\\<rat>', 'ℚ'),
    ('\\<real>', 'ℝ'),
    ('\\<int>', 'ℤ'),
    ('\\<leftarrow>', '←'),
    ('\\<longleftarrow>', '⟵'),
    ('\\<rightarrow>', '→'),
    ('\\<longrightarrow>', '⟶'),
    ('\\<Leftarrow>', '⇐'),
    ('\\<Longleftarrow>', '⟸'),
    ('\\<Rightarrow>', '⇒'),
    ('\\<Longrightarrow>', '⟹'),
    ('\\<leftrightarrow>', '↔'),
    ('\\<longleftrightarrow>', '⟷'),
    ('\\<Leftrightarrow>', '⇔'),
    ('\\<Longleftrightarrow>', '⟺'),
    ('\\<mapsto>', '↦'),
    ('\\<longmapsto>', '⟼'),
    ('\\<midarrow>', '─'),
    ('\\<Midarrow>', '═'),
    ('\\<hookleftarrow>', '↩'),
    ('\\<hookrightarrow>', '↪'),
    ('\\<leftharpoondown>', '↽'),
    ('\\<rightharpoondown>', '⇁'),
    ('\\<leftharpoonup>', '↼'),
    ('\\<rightharpoonup>', '⇀'),
    ('\\<rightleftharpoons>', '⇌'),
    ('\\<leadsto>', '↝'),
    ('\\<downharpoonleft>', '⇃'),
    ('\\<downharpoonright>', '⇂'),
    ('\\<upharpoonleft>', '↿'),
    ('\\<restriction>', '↾'),
    ('\\<Colon>', '∷'),
    ('\\<up>', '↑'),
    ('\\<Up>', '⇑'),
    ('\\<down>', '↓'),
    ('\\<Down>', '⇓'),
    ('\\<updown>', '↕'),
    ('\\<Updown>', '⇕'),
    ('\\<langle>', '⟨'),
    ('\\<rangle>', '⟩'),
    ('\\<lceil>', '⌈'),
    ('\\<rceil>', '⌉'),
    ('\\<lfloor>', '⌊'),
    ('\\<rfloor>', '⌋'),
    ('\\<lparr>', '⦇'),
    ('\\<rparr>', '⦈'),
    ('\\<lbrakk>', '⟦'),
    ('\\<rbrakk>', '⟧'),
    ('\\<lbrace>', '⦃'),
    ('\\<rbrace>', '⦄'),
    ('\\<guillemotleft>', '«'),
    ('\\<guillemotright>', '»'),
    ('\\<bottom>', '⊥'),
    ('\\<top>', '⊤'),
    ('\\<and>', '∧'),
    ('\\<And>', '⋀'),
    ('\\<or>', '∨'),
    ('\\<Or>', '⋁'),
    ('\\<forall>', '∀'),
    ('\\<exists>', '∃'),
    ('\\<nexists>', '∄'),
    ('\\<not>', '¬'),
    ('\\<box>', '□'),
    ('\\<diamond>', '◇'),
    ('\\<turnstile>', '⊢'),
    ('\\<Turnstile>', '⊨'),
    ('\\<tturnstile>', '⊩'),
    ('\\<TTurnstile>', '⊫'),
    ('\\<stileturn>', '⊣'),
    ('\\<surd>', '√'),
    ('\\<le>', '≤'),
    ('\\<ge>', '≥'),
    ('\\<lless>', '≪'),
    ('\\<ggreater>', '≫'),
    ('\\<lesssim>', '≲'),
    ('\\<greatersim>', '≳'),
    ('\\<lessapprox>', '⪅'),
    ('\\<greaterapprox>', '⪆'),
    ('\\<in>', '∈'),
    ('\\<notin>', '∉'),
    ('\\<subset>', '⊂'),
    ('\\<supset>', '⊃'),
    ('\\<subseteq>', '⊆'),
    ('\\<supseteq>', '⊇'),
    ('\\<sqsubset>', '⊏'),
    ('\\<sqsupset>', '⊐'),
    ('\\<sqsubseteq>', '⊑'),
    ('\\<sqsupseteq>', '⊒'),
    ('\\<inter>', '∩'),
    ('\\<Inter>', '⋂'),
    ('\\<union>', '∪'),
    ('\\<Union>', '⋃'),
    ('\\<squnion>', '⊔'),
    ('\\<Squnion>', '⨆'),
    ('\\<sqinter>', '⊓'),
    ('\\<Sqinter>', '⨅'),
    ('\\<setminus>', '∖'),
    ('\\<propto>', '∝'),
    ('\\<uplus>', '⊎'),
    ('\\<Uplus>', '⨄'),
    ('\\<noteq>', '≠'),
    ('\\<sim>', '∼'),
    ('\\<doteq>', '≐'),
    ('\\<simeq>', '≃'),
    ('\\<approx>', '≈'),
    ('\\<asymp>', '≍'),
    ('\\<cong>', '≅'),
    ('\\<smile>', '⌣'),
    ('\\<equiv>', '≡'),
    ('\\<frown>', '⌢'),
    ('\\<Join>', '⋈'),
    ('\\<bowtie>', '⨝'),
    ('\\<prec>', '≺'),
    ('\\<succ>', '≻'),
    ('\\<preceq>', '≼'),
    ('\\<succeq>', '≽'),
    ('\\<parallel>', '∥'),
    ('\\<bar>', '¦'),
    ('\\<plusminus>', '±'),
    ('\\<minusplus>', '∓'),
    ('\\<times>', '×'),
    ('\\<div>', '÷'),
    ('\\<cdot>', '⋅'),
    ('\\<star>', '⋆'),
    ('\\<bullet>', '∙'),
    ('\\<circ>', '∘'),
    ('\\<dagger>', '†'),
    ('\\<ddagger>', '‡'),
    ('\\<lhd>', '⊲'),
    ('\\<rhd>', '⊳'),
    ('\\<unlhd>', '⊴'),
    ('\\<unrhd>', '⊵'),
    ('\\<triangleleft>', '◃'),
    ('\\<triangleright>', '▹'),
    ('\\<triangle>', '△'),
    ('\\<triangleq>', '≜'),
    ('\\<oplus>', '⊕'),
    ('\\<Oplus>', '⨁'),
    ('\\<otimes>', '⊗'),
    ('\\<Otimes>', '⨂'),
    ('\\<odot>', '⊙'),
    ('\\<Odot>', '⨀'),
    ('\\<ominus>', '⊖'),
    ('\\<oslash>', '⊘'),
    ('\\<dots>', '…'),
    ('\\<cdots>', '⋯'),
    ('\\<Sum>', '∑'),
    ('\\<Prod>', '∏'),
    ('\\<Coprod>', '∐'),
    ('\\<infinity>', '∞'),
    ('\\<integral>', '∫'),
    ('\\<ointegral>', '∮'),
    ('\\<clubsuit>', '♣'),
    ('\\<diamondsuit>', '♢'),
    ('\\<heartsuit>', '♡'),
    ('\\<spadesuit>', '♠'),
    ('\\<aleph>', 'ℵ'),
    ('\\<emptyset>', '∅'),
    ('\\<nabla>', '∇'),
    ('\\<partial>', '∂'),
    ('\\<flat>', '♭'),
    ('\\<natural>', '♮'),
    ('\\<sharp>', '♯'),
    ('\\<angle>', '∠'),
    ('\\<copyright>', '©'),
    ('\\<registered>', '®'),
    ('\\<hyphen>', '­'),
    ('\\<inverse>', '¯'),
    ('\\<onequarter>', '¼'),
    ('\\<onehalf>', '½'),
    ('\\<threequarters>', '¾'),
    ('\\<ordfeminine>', 'ª'),
    ('\\<ordmasculine>', 'º'),
    ('\\<section>', '§'),
    ('\\<paragraph>', '¶'),
    ('\\<exclamdown>', '¡'),
    ('\\<questiondown>', '¿'),
    ('\\<euro>', '€'),
    ('\\<pounds>', '£'),
    ('\\<yen>', '¥'),
    ('\\<cent>', '¢'),
    ('\\<currency>', '¤'),
    ('\\<degree>', '°'),
    ('\\<amalg>', '⨿'),
    ('\\<mho>', '℧'),
    ('\\<lozenge>', '◊'),
    ('\\<wp>', '℘'),
    ('\\<wrong>', '≀'),
    ('\\<struct>', '⋄'),
    ('\\<acute>', '´'),
    ('\\<index>', 'ı'),
    ('\\<dieresis>', '¨'),
    ('\\<cedilla>', '¸'),
    ('\\<hungarumlaut>', '˝'),
    ('\\<some>', 'ϵ'),
    ('\\<hole>', '⌑'),
    ('\\<newline>', '⏎'),
    ('\\<open>', '‹'),
    ('\\<close>', '›'),
    ('\\<here>', '⌂'),
    ('\\<^sub>', '⇩'),
    ('\\<^sup>', '⇧'),
    ('\\<^bold>', '❙'),
    ('\\<^bsub>', '⇘'),
    ('\\<^esub>', '⇙'),
    ('\\<^bsup>', '⇗'),
    ('\\<^esup>', '⇖'),
))
