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