1#!/usr/bin/env python 2# -*- coding: utf-8 -*- 3# 4# Copyright 2017, Data61 5# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 6# ABN 41 687 119 230. 7# 8# This software may be distributed and modified according to the terms of 9# the BSD 2-Clause license. Note that NO WARRANTY is provided. 10# See "LICENSE_BSD2.txt" for details. 11# 12# @TAG(DATA61_BSD) 13# 14 15# THIS FILE WAS GENERATED BY make_isabelle_symbols.py. 16 17from __future__ import absolute_import, division, print_function, \ 18 unicode_literals 19from camkes.internal.seven import cmp, filter, map, zip 20 21ISABELLE_SYMBOLS = frozenset(( 22 ('\\<zero>', '����'), 23 ('\\<one>', '����'), 24 ('\\<two>', '����'), 25 ('\\<three>', '����'), 26 ('\\<four>', '����'), 27 ('\\<five>', '����'), 28 ('\\<six>', '����'), 29 ('\\<seven>', '����'), 30 ('\\<eight>', '����'), 31 ('\\<nine>', '����'), 32 ('\\<A>', '����'), 33 ('\\<B>', '���'), 34 ('\\<C>', '����'), 35 ('\\<D>', '����'), 36 ('\\<E>', '���'), 37 ('\\<F>', '���'), 38 ('\\<G>', '����'), 39 ('\\<H>', '���'), 40 ('\\<I>', '���'), 41 ('\\<J>', '����'), 42 ('\\<K>', '����'), 43 ('\\<L>', '���'), 44 ('\\<M>', '���'), 45 ('\\<N>', '����'), 46 ('\\<O>', '����'), 47 ('\\<P>', '����'), 48 ('\\<Q>', '����'), 49 ('\\<R>', '���'), 50 ('\\<S>', '����'), 51 ('\\<T>', '����'), 52 ('\\<U>', '����'), 53 ('\\<V>', '����'), 54 ('\\<W>', '����'), 55 ('\\<X>', '����'), 56 ('\\<Y>', '����'), 57 ('\\<Z>', '����'), 58 ('\\<a>', '����'), 59 ('\\<b>', '����'), 60 ('\\<c>', '����'), 61 ('\\<d>', '����'), 62 ('\\<e>', '����'), 63 ('\\<f>', '����'), 64 ('\\<g>', '����'), 65 ('\\<h>', '����'), 66 ('\\<i>', '����'), 67 ('\\<j>', '����'), 68 ('\\<k>', '����'), 69 ('\\<l>', '����'), 70 ('\\<m>', '����'), 71 ('\\<n>', '����'), 72 ('\\<o>', '����'), 73 ('\\<p>', '����'), 74 ('\\<q>', '����'), 75 ('\\<r>', '����'), 76 ('\\<s>', '����'), 77 ('\\<t>', '����'), 78 ('\\<u>', '����'), 79 ('\\<v>', '����'), 80 ('\\<w>', '����'), 81 ('\\<x>', '����'), 82 ('\\<y>', '����'), 83 ('\\<z>', '����'), 84 ('\\<AA>', '����'), 85 ('\\<BB>', '����'), 86 ('\\<CC>', '���'), 87 ('\\<DD>', '����'), 88 ('\\<EE>', '����'), 89 ('\\<FF>', '����'), 90 ('\\<GG>', '����'), 91 ('\\<HH>', '���'), 92 ('\\<II>', '���'), 93 ('\\<JJ>', '����'), 94 ('\\<KK>', '����'), 95 ('\\<LL>', '����'), 96 ('\\<MM>', '����'), 97 ('\\<NN>', '����'), 98 ('\\<OO>', '����'), 99 ('\\<PP>', '����'), 100 ('\\<QQ>', '����'), 101 ('\\<RR>', '���'), 102 ('\\<SS>', '����'), 103 ('\\<TT>', '����'), 104 ('\\<UU>', '����'), 105 ('\\<VV>', '����'), 106 ('\\<WW>', '����'), 107 ('\\<XX>', '����'), 108 ('\\<YY>', '����'), 109 ('\\<ZZ>', '���'), 110 ('\\<aa>', '����'), 111 ('\\<bb>', '����'), 112 ('\\<cc>', '����'), 113 ('\\<dd>', '����'), 114 ('\\<ee>', '����'), 115 ('\\<ff>', '����'), 116 ('\\<gg>', '����'), 117 ('\\<hh>', '����'), 118 ('\\<ii>', '����'), 119 ('\\<jj>', '����'), 120 ('\\<kk>', '����'), 121 ('\\<ll>', '����'), 122 ('\\<mm>', '����'), 123 ('\\<nn>', '����'), 124 ('\\<oo>', '����'), 125 ('\\<pp>', '����'), 126 ('\\<qq>', '����'), 127 ('\\<rr>', '����'), 128 ('\\<ss>', '����'), 129 ('\\<tt>', '����'), 130 ('\\<uu>', '����'), 131 ('\\<vv>', '����'), 132 ('\\<ww>', '����'), 133 ('\\<xx>', '����'), 134 ('\\<yy>', '����'), 135 ('\\<zz>', '����'), 136 ('\\<alpha>', '��'), 137 ('\\<beta>', '��'), 138 ('\\<gamma>', '��'), 139 ('\\<delta>', '��'), 140 ('\\<epsilon>', '��'), 141 ('\\<zeta>', '��'), 142 ('\\<eta>', '��'), 143 ('\\<theta>', '��'), 144 ('\\<iota>', '��'), 145 ('\\<kappa>', '��'), 146 ('\\<lambda>', '��'), 147 ('\\<mu>', '��'), 148 ('\\<nu>', '��'), 149 ('\\<xi>', '��'), 150 ('\\<pi>', '��'), 151 ('\\<rho>', '��'), 152 ('\\<sigma>', '��'), 153 ('\\<tau>', '��'), 154 ('\\<upsilon>', '��'), 155 ('\\<phi>', '��'), 156 ('\\<chi>', '��'), 157 ('\\<psi>', '��'), 158 ('\\<omega>', '��'), 159 ('\\<Gamma>', '��'), 160 ('\\<Delta>', '��'), 161 ('\\<Theta>', '��'), 162 ('\\<Lambda>', '��'), 163 ('\\<Xi>', '��'), 164 ('\\<Pi>', '��'), 165 ('\\<Sigma>', '��'), 166 ('\\<Upsilon>', '��'), 167 ('\\<Phi>', '��'), 168 ('\\<Psi>', '��'), 169 ('\\<Omega>', '��'), 170 ('\\<bool>', '����'), 171 ('\\<complex>', '���'), 172 ('\\<nat>', '���'), 173 ('\\<rat>', '���'), 174 ('\\<real>', '���'), 175 ('\\<int>', '���'), 176 ('\\<leftarrow>', '���'), 177 ('\\<longleftarrow>', '���'), 178 ('\\<rightarrow>', '���'), 179 ('\\<longrightarrow>', '���'), 180 ('\\<Leftarrow>', '���'), 181 ('\\<Longleftarrow>', '���'), 182 ('\\<Rightarrow>', '���'), 183 ('\\<Longrightarrow>', '���'), 184 ('\\<leftrightarrow>', '���'), 185 ('\\<longleftrightarrow>', '���'), 186 ('\\<Leftrightarrow>', '���'), 187 ('\\<Longleftrightarrow>', '���'), 188 ('\\<mapsto>', '���'), 189 ('\\<longmapsto>', '���'), 190 ('\\<midarrow>', '���'), 191 ('\\<Midarrow>', '���'), 192 ('\\<hookleftarrow>', '���'), 193 ('\\<hookrightarrow>', '���'), 194 ('\\<leftharpoondown>', '���'), 195 ('\\<rightharpoondown>', '���'), 196 ('\\<leftharpoonup>', '���'), 197 ('\\<rightharpoonup>', '���'), 198 ('\\<rightleftharpoons>', '���'), 199 ('\\<leadsto>', '���'), 200 ('\\<downharpoonleft>', '���'), 201 ('\\<downharpoonright>', '���'), 202 ('\\<upharpoonleft>', '���'), 203 ('\\<restriction>', '���'), 204 ('\\<Colon>', '���'), 205 ('\\<up>', '���'), 206 ('\\<Up>', '���'), 207 ('\\<down>', '���'), 208 ('\\<Down>', '���'), 209 ('\\<updown>', '���'), 210 ('\\<Updown>', '���'), 211 ('\\<langle>', '���'), 212 ('\\<rangle>', '���'), 213 ('\\<lceil>', '���'), 214 ('\\<rceil>', '���'), 215 ('\\<lfloor>', '���'), 216 ('\\<rfloor>', '���'), 217 ('\\<lparr>', '���'), 218 ('\\<rparr>', '���'), 219 ('\\<lbrakk>', '���'), 220 ('\\<rbrakk>', '���'), 221 ('\\<lbrace>', '���'), 222 ('\\<rbrace>', '���'), 223 ('\\<guillemotleft>', '��'), 224 ('\\<guillemotright>', '��'), 225 ('\\<bottom>', '���'), 226 ('\\<top>', '���'), 227 ('\\<and>', '���'), 228 ('\\<And>', '���'), 229 ('\\<or>', '���'), 230 ('\\<Or>', '���'), 231 ('\\<forall>', '���'), 232 ('\\<exists>', '���'), 233 ('\\<nexists>', '���'), 234 ('\\<not>', '��'), 235 ('\\<box>', '���'), 236 ('\\<diamond>', '���'), 237 ('\\<turnstile>', '���'), 238 ('\\<Turnstile>', '���'), 239 ('\\<tturnstile>', '���'), 240 ('\\<TTurnstile>', '���'), 241 ('\\<stileturn>', '���'), 242 ('\\<surd>', '���'), 243 ('\\<le>', '���'), 244 ('\\<ge>', '���'), 245 ('\\<lless>', '���'), 246 ('\\<ggreater>', '���'), 247 ('\\<lesssim>', '���'), 248 ('\\<greatersim>', '���'), 249 ('\\<lessapprox>', '���'), 250 ('\\<greaterapprox>', '���'), 251 ('\\<in>', '���'), 252 ('\\<notin>', '���'), 253 ('\\<subset>', '���'), 254 ('\\<supset>', '���'), 255 ('\\<subseteq>', '���'), 256 ('\\<supseteq>', '���'), 257 ('\\<sqsubset>', '���'), 258 ('\\<sqsupset>', '���'), 259 ('\\<sqsubseteq>', '���'), 260 ('\\<sqsupseteq>', '���'), 261 ('\\<inter>', '���'), 262 ('\\<Inter>', '���'), 263 ('\\<union>', '���'), 264 ('\\<Union>', '���'), 265 ('\\<squnion>', '���'), 266 ('\\<Squnion>', '���'), 267 ('\\<sqinter>', '���'), 268 ('\\<Sqinter>', '���'), 269 ('\\<setminus>', '���'), 270 ('\\<propto>', '���'), 271 ('\\<uplus>', '���'), 272 ('\\<Uplus>', '���'), 273 ('\\<noteq>', '���'), 274 ('\\<sim>', '���'), 275 ('\\<doteq>', '���'), 276 ('\\<simeq>', '���'), 277 ('\\<approx>', '���'), 278 ('\\<asymp>', '���'), 279 ('\\<cong>', '���'), 280 ('\\<smile>', '���'), 281 ('\\<equiv>', '���'), 282 ('\\<frown>', '���'), 283 ('\\<Join>', '���'), 284 ('\\<bowtie>', '���'), 285 ('\\<prec>', '���'), 286 ('\\<succ>', '���'), 287 ('\\<preceq>', '���'), 288 ('\\<succeq>', '���'), 289 ('\\<parallel>', '���'), 290 ('\\<bar>', '��'), 291 ('\\<plusminus>', '��'), 292 ('\\<minusplus>', '���'), 293 ('\\<times>', '��'), 294 ('\\<div>', '��'), 295 ('\\<cdot>', '���'), 296 ('\\<star>', '���'), 297 ('\\<bullet>', '���'), 298 ('\\<circ>', '���'), 299 ('\\<dagger>', '���'), 300 ('\\<ddagger>', '���'), 301 ('\\<lhd>', '���'), 302 ('\\<rhd>', '���'), 303 ('\\<unlhd>', '���'), 304 ('\\<unrhd>', '���'), 305 ('\\<triangleleft>', '���'), 306 ('\\<triangleright>', '���'), 307 ('\\<triangle>', '���'), 308 ('\\<triangleq>', '���'), 309 ('\\<oplus>', '���'), 310 ('\\<Oplus>', '���'), 311 ('\\<otimes>', '���'), 312 ('\\<Otimes>', '���'), 313 ('\\<odot>', '���'), 314 ('\\<Odot>', '���'), 315 ('\\<ominus>', '���'), 316 ('\\<oslash>', '���'), 317 ('\\<dots>', '���'), 318 ('\\<cdots>', '���'), 319 ('\\<Sum>', '���'), 320 ('\\<Prod>', '���'), 321 ('\\<Coprod>', '���'), 322 ('\\<infinity>', '���'), 323 ('\\<integral>', '���'), 324 ('\\<ointegral>', '���'), 325 ('\\<clubsuit>', '���'), 326 ('\\<diamondsuit>', '���'), 327 ('\\<heartsuit>', '���'), 328 ('\\<spadesuit>', '���'), 329 ('\\<aleph>', '���'), 330 ('\\<emptyset>', '���'), 331 ('\\<nabla>', '���'), 332 ('\\<partial>', '���'), 333 ('\\<flat>', '���'), 334 ('\\<natural>', '���'), 335 ('\\<sharp>', '���'), 336 ('\\<angle>', '���'), 337 ('\\<copyright>', '��'), 338 ('\\<registered>', '��'), 339 ('\\<hyphen>', '��'), 340 ('\\<inverse>', '��'), 341 ('\\<onequarter>', '��'), 342 ('\\<onehalf>', '��'), 343 ('\\<threequarters>', '��'), 344 ('\\<ordfeminine>', '��'), 345 ('\\<ordmasculine>', '��'), 346 ('\\<section>', '��'), 347 ('\\<paragraph>', '��'), 348 ('\\<exclamdown>', '��'), 349 ('\\<questiondown>', '��'), 350 ('\\<euro>', '���'), 351 ('\\<pounds>', '��'), 352 ('\\<yen>', '��'), 353 ('\\<cent>', '��'), 354 ('\\<currency>', '��'), 355 ('\\<degree>', '��'), 356 ('\\<amalg>', '���'), 357 ('\\<mho>', '���'), 358 ('\\<lozenge>', '���'), 359 ('\\<wp>', '���'), 360 ('\\<wrong>', '���'), 361 ('\\<struct>', '���'), 362 ('\\<acute>', '��'), 363 ('\\<index>', '��'), 364 ('\\<dieresis>', '��'), 365 ('\\<cedilla>', '��'), 366 ('\\<hungarumlaut>', '��'), 367 ('\\<some>', '��'), 368 ('\\<hole>', '���'), 369 ('\\<newline>', '���'), 370 ('\\<open>', '���'), 371 ('\\<close>', '���'), 372 ('\\<here>', '���'), 373 ('\\<^sub>', '���'), 374 ('\\<^sup>', '���'), 375 ('\\<^bold>', '���'), 376 ('\\<^bsub>', '���'), 377 ('\\<^esub>', '���'), 378 ('\\<^bsup>', '���'), 379 ('\\<^esup>', '���'), 380)) 381