2943

1 
#


2 
# $Id$

2397

3 
#

2943

4 
# symbolinput.pl  expand isabelle0 encoded chars to \<...> sequences.


5 
#

2397

6 


7 
%tab = (

2943

8 
#GENERATED TEXT FOLLOWS  Do not edit!

3064

9 
"\x91", "\\<lless>",


10 
"\x92", "\\<unlhd>",


11 
"\x93", "\\<lhd>",


12 
"\x94", "\\<rhd>",


13 
"\x95", "\\<tturnstile>",


14 
"\x96", "\\<langle>",


15 
"\x97", "\\<rangle>",

3067

16 
"\x98", "\\<orelse>",

3064

17 
"\x99", "\\<top>",


18 
"\x9a", "\\<Or>",


19 
"\x9b", "\\<ocdot>",


20 
"\x9c", "\\<iota>",


21 
"\x9d", "\\<upsilon>",


22 
"\x9e", "\\<Upsilon>",


23 
"\x9f", "\\<Xi>",


24 
"\xa0", "\\<space2>",

2945

25 
"\xa1", "\\<Gamma>",


26 
"\xa2", "\\<Delta>",


27 
"\xa3", "\\<Theta>",


28 
"\xa4", "\\<Lambda>",


29 
"\xa5", "\\<Pi>",


30 
"\xa6", "\\<Sigma>",


31 
"\xa7", "\\<Phi>",


32 
"\xa8", "\\<Psi>",


33 
"\xa9", "\\<Omega>",


34 
"\xaa", "\\<alpha>",


35 
"\xab", "\\<beta>",


36 
"\xac", "\\<gamma>",


37 
"\xad", "\\<delta>",


38 
"\xae", "\\<epsilon>",


39 
"\xaf", "\\<zeta>",


40 
"\xb0", "\\<eta>",


41 
"\xb1", "\\<theta>",


42 
"\xb2", "\\<kappa>",


43 
"\xb3", "\\<lambda>",


44 
"\xb4", "\\<mu>",


45 
"\xb5", "\\<nu>",


46 
"\xb6", "\\<xi>",


47 
"\xb7", "\\<pi>",


48 
"\xb8", "\\<rho>",


49 
"\xb9", "\\<sigma>",


50 
"\xba", "\\<tau>",


51 
"\xbb", "\\<phi>",


52 
"\xbc", "\\<chi>",


53 
"\xbd", "\\<psi>",


54 
"\xbe", "\\<omega>",


55 
"\xbf", "\\<not>",


56 
"\xc0", "\\<and>",


57 
"\xc1", "\\<or>",


58 
"\xc2", "\\<forall>",


59 
"\xc3", "\\<exists>",


60 
"\xc4", "\\<And>",

3064

61 
"\xc5", "\\<lceil>",


62 
"\xc6", "\\<rceil>",


63 
"\xc7", "\\<lfloor>",


64 
"\xc8", "\\<rfloor>",

2945

65 
"\xc9", "\\<turnstile>",


66 
"\xca", "\\<Turnstile>",


67 
"\xcb", "\\<lbrakk>",


68 
"\xcc", "\\<rbrakk>",


69 
"\xcd", "\\<cdot>",


70 
"\xce", "\\<in>",


71 
"\xcf", "\\<subseteq>",


72 
"\xd0", "\\<inter>",


73 
"\xd1", "\\<union>",


74 
"\xd2", "\\<Inter>",


75 
"\xd3", "\\<Union>",


76 
"\xd4", "\\<sqinter>",


77 
"\xd5", "\\<squnion>",


78 
"\xd6", "\\<Sqinter>",


79 
"\xd7", "\\<Squnion>",


80 
"\xd8", "\\<bottom>",


81 
"\xd9", "\\<doteq>",


82 
"\xda", "\\<equiv>",


83 
"\xdb", "\\<noteq>",


84 
"\xdc", "\\<sqsubset>",


85 
"\xdd", "\\<sqsubseteq>",


86 
"\xde", "\\<prec>",


87 
"\xdf", "\\<preceq>",


88 
"\xe0", "\\<succ>",


89 
"\xe1", "\\<approx>",


90 
"\xe2", "\\<sim>",


91 
"\xe3", "\\<simeq>",


92 
"\xe4", "\\<le>",


93 
"\xe5", "\\<Colon>",


94 
"\xe6", "\\<leftarrow>",


95 
"\xe7", "\\<midarrow>",


96 
"\xe8", "\\<rightarrow>",


97 
"\xe9", "\\<Leftarrow>",


98 
"\xea", "\\<Midarrow>",


99 
"\xeb", "\\<Rightarrow>",


100 
"\xec", "\\<bow>",


101 
"\xed", "\\<mapsto>",


102 
"\xee", "\\<leadsto>",


103 
"\xef", "\\<up>",


104 
"\xf0", "\\<down>",


105 
"\xf1", "\\<notin>",


106 
"\xf2", "\\<times>",


107 
"\xf3", "\\<oplus>",


108 
"\xf4", "\\<ominus>",


109 
"\xf5", "\\<otimes>",


110 
"\xf6", "\\<oslash>",


111 
"\xf7", "\\<subset>",


112 
"\xf8", "\\<infinity>",


113 
"\xf9", "\\<box>",


114 
"\xfa", "\\<diamond>",


115 
"\xfb", "\\<circ>",


116 
"\xfc", "\\<bullet>",


117 
"\xfd", "\\<parallel>",


118 
"\xfe", "\\<surd>",


119 
"\xff", "\\<copyright>"

2943

120 
#END OF GENERATED TEXT


121 
);

2397

122 


123 
$SIG{INT} = "IGNORE";


124 
$ = 1;


125 


126 
while (<ARGV>) {

2943

127 
s/([\xa1\xff])/\\$tab{$1}/g;

2397

128 
print;


129 
}
