588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder '\o377', '^', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0',
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder '�', '!', '�', '$', '&', '/', '(', ')', '=', '?', '\\' : s
. true %(The true formula)%
and with special stuff: -*/\&=<>BCDEFGHIJKLM!% )%
op c : s � s -> s,assoc, comm, idem, unit a; c : s � s � s -> s
op c : s � s ->? s,assoc, comm, idem, unit a
op c(x : s; y : s; z : t) : s = a
op c(x : s; y : s; z : t) :? s = a
predfun c : s � s ->? Unit; c : s � s � s ->? Unit
predfun c(x : s; y : s; z : t) :? Unit = false
type Data2 ::= Cons21 (Data1; Data2) |
type Data3 ::= Cons31 (sel1:? Data1; sel2:? Data2) |
Cons32 (sel2:? Data2; sel1:? Data1)
type Data4 ::= Cons41 (sel1:? Data1; sel2:? Data2) ? |
Cons42 (sel2:? Data2; sel1:? Data1) ?
type Tree ::= Leaf (Data1) |
generated {type Set ::= Mt |
generated {type Set ::= Mt |
generated {type nat; op 0 : nat; succ : nat -> nat}
op f, g : s ->? s; g : s -> t;
__+__, __-__, __*__, __/__ : s � s -> s; {} : s; {__} : s -> s
predfun p : Unit; q : s ->? Unit
var x : s; y : s; z : s; r1 : t; r2 : t
. not p /\ not q (x) /\ q (x)
. not p \/ not q (x) \/ q (x)
. not p /\ not q (x) /\ q (x) => not p \/ not q (x) \/ q (x) => not
. not p /\ not q (x) /\ q (x)
not p \/ not q (x) \/ q (x)
not p /\ not q (x) /\ q (x)
forall x : s . not p /\ not q (x) /\ q (x) <=>
exists x : s . not p \/ not q (x) \/ q (x) <=>
exists! x : s . not p /\ not q (x) /\ q (x)
. def (op f : s ->? s) (x)
. def (op g : s -> t) (x)
. (predfun q : s ->? Unit) (x)
. def x * y * z + z * y * x
free type Boolean ::= True |
op Not__ : Boolean -> Boolean;
__And__, __Or__ : Boolean � Boolean -> Boolean
forall x : Boolean; y : Boolean; z : Boolean
. Not (False) = True %(Not_False)%
. Not (True) = False %(Not_True)%
. False And False = False %(And_def1)%
. False And True = False %(And_def2)%
. True And False = False %(And_def3)%
. True And True = True %(And_def4)%
. x Or y = Not (Not (x) And Not (y)) %(Or_def)%
op chr : Nat ->? Char; ord : Char -> Nat
. def chr (n) <=> n <= 255 %(chr_dom)%
. chr (ord (c)) = c %(chr_def)%
. ord (chr (n)) = n if n <= 255 %(ord_def)%
%% definition of individual characters:
op '\000' : Char = chr (0) %(slash_000)%;
'\001' : Char = chr (1) %(slash_001)%;
'\002' : Char = chr (2) %(slash_002)%;
'\003' : Char = chr (3) %(slash_003)%;
'\004' : Char = chr (4) %(slash_004)%;
'\005' : Char = chr (5) %(slash_005)%;
'\006' : Char = chr (6) %(slash_006)%;
'\007' : Char = chr (7) %(slash_007)%;
'\008' : Char = chr (8) %(slash_008)%;
'\009' : Char = chr (9) %(slash_009)%;
'\010' : Char = chr (10) %(slash_010)%;
'\011' : Char = chr (11) %(slash_011)%;
'\012' : Char = chr (12) %(slash_012)%;
'\013' : Char = chr (13) %(slash_013)%;
'\014' : Char = chr (14) %(slash_014)%;
'\015' : Char = chr (15) %(slash_015)%;
'\016' : Char = chr (16) %(slash_016)%;
'\017' : Char = chr (17) %(slash_017)%;
'\018' : Char = chr (18) %(slash_018)%;
'\019' : Char = chr (19) %(slash_019)%;
'\020' : Char = chr (20) %(slash_020)%;
'\021' : Char = chr (21) %(slash_021)%;
'\022' : Char = chr (22) %(slash_022)%;
'\023' : Char = chr (23) %(slash_023)%;
'\024' : Char = chr (24) %(slash_024)%;
'\025' : Char = chr (25) %(slash_025)%;
'\026' : Char = chr (26) %(slash_026)%;
'\027' : Char = chr (27) %(slash_027)%;
'\028' : Char = chr (28) %(slash_028)%;
'\029' : Char = chr (29) %(slash_029)%;
'\030' : Char = chr (30) %(slash_030)%;
'\031' : Char = chr (31) %(slash_031)%;
'\032' : Char = chr (32) %(slash_032)%;
'\033' : Char = chr (33) %(slash_033)%;
'\034' : Char = chr (34) %(slash_034)%;
'\035' : Char = chr (35) %(slash_035)%;
'\036' : Char = chr (36) %(slash_036)%;
'\037' : Char = chr (37) %(slash_037)%;
'\038' : Char = chr (38) %(slash_038)%;
'\039' : Char = chr (39) %(slash_039)%;
'\040' : Char = chr (40) %(slash_040)%;
'\041' : Char = chr (41) %(slash_041)%;
'\042' : Char = chr (42) %(slash_042)%;
'\043' : Char = chr (43) %(slash_043)%;
'\044' : Char = chr (44) %(slash_044)%;
'\045' : Char = chr (45) %(slash_045)%;
'\046' : Char = chr (46) %(slash_046)%;
'\047' : Char = chr (47) %(slash_047)%;
'\048' : Char = chr (48) %(slash_048)%;
'\049' : Char = chr (49) %(slash_049)%;
'\050' : Char = chr (50) %(slash_050)%;
'\051' : Char = chr (51) %(slash_051)%;
'\052' : Char = chr (52) %(slash_052)%;
'\053' : Char = chr (53) %(slash_053)%;
'\054' : Char = chr (54) %(slash_054)%;
'\055' : Char = chr (55) %(slash_055)%;
'\056' : Char = chr (56) %(slash_056)%;
'\057' : Char = chr (57) %(slash_057)%;
'\058' : Char = chr (58) %(slash_058)%;
'\059' : Char = chr (59) %(slash_059)%;
'\060' : Char = chr (60) %(slash_060)%;
'\061' : Char = chr (61) %(slash_061)%;
'\062' : Char = chr (62) %(slash_062)%;
'\063' : Char = chr (63) %(slash_063)%;
'\064' : Char = chr (64) %(slash_064)%;
'\065' : Char = chr (65) %(slash_065)%;
'\066' : Char = chr (66) %(slash_066)%;
'\067' : Char = chr (67) %(slash_067)%;
'\068' : Char = chr (68) %(slash_068)%;
'\069' : Char = chr (69) %(slash_069)%;
'\070' : Char = chr (70) %(slash_070)%;
'\071' : Char = chr (71) %(slash_071)%;
'\072' : Char = chr (72) %(slash_072)%;
'\073' : Char = chr (73) %(slash_073)%;
'\074' : Char = chr (74) %(slash_074)%;
'\075' : Char = chr (75) %(slash_075)%;
'\076' : Char = chr (76) %(slash_076)%;
'\077' : Char = chr (77) %(slash_077)%;
'\078' : Char = chr (78) %(slash_078)%;
'\079' : Char = chr (79) %(slash_079)%;
'\080' : Char = chr (80) %(slash_080)%;
'\081' : Char = chr (81) %(slash_081)%;
'\082' : Char = chr (82) %(slash_082)%;
'\083' : Char = chr (83) %(slash_083)%;
'\084' : Char = chr (84) %(slash_084)%;
'\085' : Char = chr (85) %(slash_085)%;
'\086' : Char = chr (86) %(slash_086)%;
'\087' : Char = chr (87) %(slash_087)%;
'\088' : Char = chr (88) %(slash_088)%;
'\089' : Char = chr (89) %(slash_089)%;
'\090' : Char = chr (90) %(slash_090)%;
'\091' : Char = chr (91) %(slash_091)%;
'\092' : Char = chr (92) %(slash_092)%;
'\093' : Char = chr (93) %(slash_093)%;
'\094' : Char = chr (94) %(slash_094)%;
'\095' : Char = chr (95) %(slash_095)%;
'\096' : Char = chr (96) %(slash_096)%;
'\097' : Char = chr (97) %(slash_097)%;
'\098' : Char = chr (98) %(slash_098)%;
'\099' : Char = chr (99) %(slash_099)%;
'\100' : Char = chr (100) %(slash_100)%;
'\101' : Char = chr (101) %(slash_101)%;
'\102' : Char = chr (102) %(slash_102)%;
'\103' : Char = chr (103) %(slash_103)%;
'\104' : Char = chr (104) %(slash_104)%;
'\105' : Char = chr (105) %(slash_105)%;
'\106' : Char = chr (106) %(slash_106)%;
'\107' : Char = chr (107) %(slash_107)%;
'\108' : Char = chr (108) %(slash_108)%;
'\109' : Char = chr (109) %(slash_109)%;
'\110' : Char = chr (110) %(slash_110)%;
'\111' : Char = chr (111) %(slash_111)%;
'\112' : Char = chr (112) %(slash_112)%;
'\113' : Char = chr (113) %(slash_113)%;
'\114' : Char = chr (114) %(slash_114)%;
'\115' : Char = chr (115) %(slash_115)%;
'\116' : Char = chr (116) %(slash_116)%;
'\117' : Char = chr (117) %(slash_117)%;
'\118' : Char = chr (118) %(slash_118)%;
'\119' : Char = chr (119) %(slash_119)%;
'\120' : Char = chr (120) %(slash_120)%;
'\121' : Char = chr (121) %(slash_121)%;
'\122' : Char = chr (122) %(slash_122)%;
'\123' : Char = chr (123) %(slash_123)%;
'\124' : Char = chr (124) %(slash_124)%;
'\125' : Char = chr (125) %(slash_125)%;
'\126' : Char = chr (126) %(slash_126)%;
'\127' : Char = chr (127) %(slash_127)%;
'\128' : Char = chr (128) %(slash_128)%;
'\129' : Char = chr (129) %(slash_129)%;
'\130' : Char = chr (130) %(slash_130)%;
'\131' : Char = chr (131) %(slash_131)%;
'\132' : Char = chr (132) %(slash_132)%;
'\133' : Char = chr (133) %(slash_133)%;
'\134' : Char = chr (134) %(slash_134)%;
'\135' : Char = chr (135) %(slash_135)%;
'\136' : Char = chr (136) %(slash_136)%;
'\137' : Char = chr (137) %(slash_137)%;
'\138' : Char = chr (138) %(slash_138)%;
'\139' : Char = chr (139) %(slash_139)%;
'\140' : Char = chr (140) %(slash_140)%;
'\141' : Char = chr (141) %(slash_141)%;
'\142' : Char = chr (142) %(slash_142)%;
'\143' : Char = chr (143) %(slash_143)%;
'\144' : Char = chr (144) %(slash_144)%;
'\145' : Char = chr (145) %(slash_145)%;
'\146' : Char = chr (146) %(slash_146)%;
'\147' : Char = chr (147) %(slash_147)%;
'\148' : Char = chr (148) %(slash_148)%;
'\149' : Char = chr (149) %(slash_149)%;
'\150' : Char = chr (150) %(slash_150)%;
'\151' : Char = chr (151) %(slash_151)%;
'\152' : Char = chr (152) %(slash_152)%;
'\153' : Char = chr (153) %(slash_153)%;
'\154' : Char = chr (154) %(slash_154)%;
'\155' : Char = chr (155) %(slash_155)%;
'\156' : Char = chr (156) %(slash_156)%;
'\157' : Char = chr (157) %(slash_157)%;
'\158' : Char = chr (158) %(slash_158)%;
'\159' : Char = chr (159) %(slash_159)%;
'\160' : Char = chr (160) %(slash_160)%;
'\161' : Char = chr (161) %(slash_161)%;
'\162' : Char = chr (162) %(slash_162)%;
'\163' : Char = chr (163) %(slash_163)%;
'\164' : Char = chr (164) %(slash_164)%;
'\165' : Char = chr (165) %(slash_165)%;
'\166' : Char = chr (166) %(slash_166)%;
'\167' : Char = chr (167) %(slash_167)%;
'\168' : Char = chr (168) %(slash_168)%;
'\169' : Char = chr (169) %(slash_169)%;
'\170' : Char = chr (170) %(slash_170)%;
'\171' : Char = chr (171) %(slash_171)%;
'\172' : Char = chr (172) %(slash_172)%;
'\173' : Char = chr (173) %(slash_173)%;
'\174' : Char = chr (174) %(slash_174)%;
'\175' : Char = chr (175) %(slash_175)%;
'\176' : Char = chr (176) %(slash_176)%;
'\177' : Char = chr (177) %(slash_177)%;
'\178' : Char = chr (178) %(slash_178)%;
'\179' : Char = chr (179) %(slash_179)%;
'\180' : Char = chr (180) %(slash_180)%;
'\181' : Char = chr (181) %(slash_181)%;
'\182' : Char = chr (182) %(slash_182)%;
'\183' : Char = chr (183) %(slash_183)%;
'\184' : Char = chr (184) %(slash_184)%;
'\185' : Char = chr (185) %(slash_185)%;
'\186' : Char = chr (186) %(slash_186)%;
'\187' : Char = chr (187) %(slash_187)%;
'\188' : Char = chr (188) %(slash_188)%;
'\189' : Char = chr (189) %(slash_189)%;
'\190' : Char = chr (190) %(slash_190)%;
'\191' : Char = chr (191) %(slash_191)%;
'\192' : Char = chr (192) %(slash_192)%;
'\193' : Char = chr (193) %(slash_193)%;
'\194' : Char = chr (194) %(slash_194)%;
'\195' : Char = chr (195) %(slash_195)%;
'\196' : Char = chr (196) %(slash_196)%;
'\197' : Char = chr (197) %(slash_197)%;
'\198' : Char = chr (198) %(slash_198)%;
'\199' : Char = chr (199) %(slash_199)%;
'\200' : Char = chr (200) %(slash_200)%;
'\201' : Char = chr (201) %(slash_201)%;
'\202' : Char = chr (202) %(slash_202)%;
'\203' : Char = chr (203) %(slash_203)%;
'\204' : Char = chr (204) %(slash_204)%;
'\205' : Char = chr (205) %(slash_205)%;
'\206' : Char = chr (206) %(slash_206)%;
'\207' : Char = chr (207) %(slash_207)%;
'\208' : Char = chr (208) %(slash_208)%;
'\209' : Char = chr (209) %(slash_209)%;
'\210' : Char = chr (210) %(slash_210)%;
'\211' : Char = chr (211) %(slash_211)%;
'\212' : Char = chr (212) %(slash_212)%;
'\213' : Char = chr (213) %(slash_213)%;
'\214' : Char = chr (214) %(slash_214)%;
'\215' : Char = chr (215) %(slash_215)%;
'\216' : Char = chr (216) %(slash_216)%;
'\217' : Char = chr (217) %(slash_217)%;
'\218' : Char = chr (218) %(slash_218)%;
'\219' : Char = chr (219) %(slash_219)%;
'\220' : Char = chr (220) %(slash_220)%;
'\221' : Char = chr (221) %(slash_221)%;
'\222' : Char = chr (222) %(slash_222)%;
'\223' : Char = chr (223) %(slash_223)%;
'\224' : Char = chr (224) %(slash_224)%;
'\225' : Char = chr (225) %(slash_225)%;
'\226' : Char = chr (226) %(slash_226)%;
'\227' : Char = chr (227) %(slash_227)%;
'\228' : Char = chr (228) %(slash_228)%;
'\229' : Char = chr (229) %(slash_229)%;
'\230' : Char = chr (230) %(slash_230)%;
'\231' : Char = chr (231) %(slash_231)%;
'\232' : Char = chr (232) %(slash_232)%;
'\233' : Char = chr (233) %(slash_233)%;
'\234' : Char = chr (234) %(slash_234)%;
'\235' : Char = chr (235) %(slash_235)%;
'\236' : Char = chr (236) %(slash_236)%;
'\237' : Char = chr (237) %(slash_237)%;
'\238' : Char = chr (238) %(slash_238)%;
'\239' : Char = chr (239) %(slash_239)%;
'\240' : Char = chr (240) %(slash_240)%;
'\241' : Char = chr (241) %(slash_241)%;
'\242' : Char = chr (242) %(slash_242)%;
'\243' : Char = chr (243) %(slash_243)%;
'\244' : Char = chr (244) %(slash_244)%;
'\245' : Char = chr (245) %(slash_245)%;
'\246' : Char = chr (246) %(slash_246)%;
'\247' : Char = chr (247) %(slash_247)%;
'\248' : Char = chr (248) %(slash_248)%;
'\249' : Char = chr (249) %(slash_249)%;
'\250' : Char = chr (250) %(slash_250)%;
'\251' : Char = chr (251) %(slash_251)%;
'\252' : Char = chr (252) %(slash_252)%;
'\253' : Char = chr (253) %(slash_253)%;
'\254' : Char = chr (254) %(slash_254)%;
'\255' : Char = chr (255) %(slash_255)%
%% definition of the printable characters:
op ' ' : Char = '\032' %(printable_32)%;
'!' : Char = '\033' %(printable_33)%;
'\"' : Char = '\034' %(printable_34)%;
'#' : Char = '\035' %(printable_35)%;
'$' : Char = '\036' %(printable_36)%;
'%' : Char = '\037' %(printable_37)%;
'&' : Char = '\038' %(printable_38)%;
'\'' : Char = '\039' %(printable_39)%;
'(' : Char = '\040' %(printable_40)%;
')' : Char = '\041' %(printable_41)%;
'*' : Char = '\042' %(printable_42)%;
'+' : Char = '\043' %(printable_43)%;
',' : Char = '\044' %(printable_44)%;
'-' : Char = '\045' %(printable_45)%;
'.' : Char = '\046' %(printable_46)%;
'/' : Char = '\047' %(printable_47)%;
'0' : Char = '\048' %(printable_48)%;
'1' : Char = '\049' %(printable_49)%;
'2' : Char = '\050' %(printable_50)%;
'3' : Char = '\051' %(printable_51)%;
'4' : Char = '\052' %(printable_52)%;
'5' : Char = '\053' %(printable_53)%;
'6' : Char = '\054' %(printable_54)%;
'7' : Char = '\055' %(printable_55)%;
'8' : Char = '\056' %(printable_56)%;
'9' : Char = '\057' %(printable_57)%;
':' : Char = '\058' %(printable_58)%;
';' : Char = '\059' %(printable_59)%;
'<' : Char = '\060' %(printable_60)%;
'=' : Char = '\061' %(printable_61)%;
'>' : Char = '\062' %(printable_62)%;
'?' : Char = '\063' %(printable_63)%;
'@' : Char = '\064' %(printable_64)%;
'A' : Char = '\065' %(printable_65)%;
'B' : Char = '\066' %(printable_66)%;
'C' : Char = '\067' %(printable_67)%;
'D' : Char = '\068' %(printable_68)%;
'E' : Char = '\069' %(printable_69)%;
'F' : Char = '\070' %(printable_70)%;
'G' : Char = '\071' %(printable_71)%;
'H' : Char = '\072' %(printable_72)%;
'I' : Char = '\073' %(printable_73)%;
'J' : Char = '\074' %(printable_74)%;
'K' : Char = '\075' %(printable_75)%;
'L' : Char = '\076' %(printable_76)%;
'M' : Char = '\077' %(printable_77)%;
'N' : Char = '\078' %(printable_78)%;
'O' : Char = '\079' %(printable_79)%;
'P' : Char = '\080' %(printable_80)%;
'Q' : Char = '\081' %(printable_81)%;
'R' : Char = '\082' %(printable_82)%;
'S' : Char = '\083' %(printable_83)%;
'T' : Char = '\084' %(printable_84)%;
'U' : Char = '\085' %(printable_85)%;
'V' : Char = '\086' %(printable_86)%;
'W' : Char = '\087' %(printable_87)%;
'X' : Char = '\088' %(printable_88)%;
'Y' : Char = '\089' %(printable_89)%;
'Z' : Char = '\090' %(printable_90)%;
'[' : Char = '\091' %(printable_91)%;
'\\' : Char = '\092' %(printable_92)%;
']' : Char = '\093' %(printable_93)%;
'^' : Char = '\094' %(printable_94)%;
'_' : Char = '\095' %(printable_95)%;
'`' : Char = '\096' %(printable_96)%;
'a' : Char = '\097' %(printable_97)%;
'b' : Char = '\098' %(printable_98)%;
'c' : Char = '\099' %(printable_99)%;
'd' : Char = '\100' %(printable_100)%;
'e' : Char = '\101' %(printable_101)%;
'f' : Char = '\102' %(printable_102)%;
'g' : Char = '\103' %(printable_103)%;
'h' : Char = '\104' %(printable_104)%;
'i' : Char = '\105' %(printable_105)%;
'j' : Char = '\106' %(printable_106)%;
'k' : Char = '\107' %(printable_107)%;
'l' : Char = '\108' %(printable_108)%;
'm' : Char = '\109' %(printable_109)%;
'n' : Char = '\110' %(printable_110)%;
'o' : Char = '\111' %(printable_111)%;
'p' : Char = '\112' %(printable_112)%;
'q' : Char = '\113' %(printable_113)%;
'r' : Char = '\114' %(printable_114)%;
's' : Char = '\115' %(printable_115)%;
't' : Char = '\116' %(printable_116)%;
'u' : Char = '\117' %(printable_117)%;
'v' : Char = '\118' %(printable_118)%;
'w' : Char = '\119' %(printable_119)%;
'x' : Char = '\120' %(printable_120)%;
'y' : Char = '\121' %(printable_121)%;
'z' : Char = '\122' %(printable_122)%;
'{' : Char = '\123' %(printable_123)%;
'|' : Char = '\124' %(printable_124)%;
'}' : Char = '\125' %(printable_125)%;
'~' : Char = '\126' %(printable_126)%;
' ' : Char = '\160' %(printable_160)%;
'�' : Char = '\161' %(printable_161)%;
'�' : Char = '\162' %(printable_162)%;
'�' : Char = '\163' %(printable_163)%;
'�' : Char = '\164' %(printable_164)%;
'�' : Char = '\165' %(printable_165)%;
'�' : Char = '\166' %(printable_166)%;
'�' : Char = '\167' %(printable_167)%;
'�' : Char = '\168' %(printable_168)%;
'�' : Char = '\169' %(printable_169)%;
'�' : Char = '\170' %(printable_170)%;
'�' : Char = '\171' %(printable_171)%;
'�' : Char = '\172' %(printable_172)%;
'�' : Char = '\173' %(printable_173)%;
'�' : Char = '\174' %(printable_174)%;
'�' : Char = '\175' %(printable_175)%;
'�' : Char = '\176' %(printable_176)%;
'�' : Char = '\177' %(printable_177)%;
'�' : Char = '\178' %(printable_178)%;
'�' : Char = '\179' %(printable_179)%;
'�' : Char = '\180' %(printable_180)%;
'�' : Char = '\181' %(printable_181)%;
'�' : Char = '\182' %(printable_182)%;
'�' : Char = '\183' %(printable_183)%;
'�' : Char = '\184' %(printable_184)%;
'�' : Char = '\185' %(printable_185)%;
'�' : Char = '\186' %(printable_186)%;
'�' : Char = '\187' %(printable_187)%;
'�' : Char = '\188' %(printable_188)%;
'�' : Char = '\189' %(printable_189)%;
'�' : Char = '\190' %(printable_190)%;
'�' : Char = '\191' %(printable_191)%;
'�' : Char = '\192' %(printable_192)%;
'�' : Char = '\193' %(printable_193)%;
'�' : Char = '\194' %(printable_194)%;
'�' : Char = '\195' %(printable_195)%;
'�' : Char = '\196' %(printable_196)%;
'�' : Char = '\197' %(printable_197)%;
'�' : Char = '\198' %(printable_198)%;
'�' : Char = '\199' %(printable_199)%;
'�' : Char = '\200' %(printable_200)%;
'�' : Char = '\201' %(printable_201)%;
'�' : Char = '\202' %(printable_202)%;
'�' : Char = '\203' %(printable_203)%;
'�' : Char = '\204' %(printable_204)%;
'�' : Char = '\205' %(printable_205)%;
'�' : Char = '\206' %(printable_206)%;
'�' : Char = '\207' %(printable_207)%;
'�' : Char = '\208' %(printable_208)%;
'�' : Char = '\209' %(printable_209)%;
'�' : Char = '\210' %(printable_210)%;
'�' : Char = '\211' %(printable_211)%;
'�' : Char = '\212' %(printable_212)%;
'�' : Char = '\213' %(printable_213)%;
'�' : Char = '\214' %(printable_214)%;
'�' : Char = '\215' %(printable_215)%;
'�' : Char = '\216' %(printable_216)%;
'�' : Char = '\217' %(printable_217)%;
'�' : Char = '\218' %(printable_218)%;
'�' : Char = '\219' %(printable_219)%;
'�' : Char = '\220' %(printable_220)%;
'�' : Char = '\221' %(printable_221)%;
'�' : Char = '\222' %(printable_222)%;
'�' : Char = '\223' %(printable_223)%;
'�' : Char = '\224' %(printable_224)%;
'�' : Char = '\225' %(printable_225)%;
'�' : Char = '\226' %(printable_226)%;
'�' : Char = '\227' %(printable_227)%;
'�' : Char = '\228' %(printable_228)%;
'�' : Char = '\229' %(printable_229)%;
'�' : Char = '\230' %(printable_230)%;
'�' : Char = '\231' %(printable_231)%;
'�' : Char = '\232' %(printable_232)%;
'�' : Char = '\233' %(printable_233)%;
'�' : Char = '\234' %(printable_234)%;
'�' : Char = '\235' %(printable_235)%;
'�' : Char = '\236' %(printable_236)%;
'�' : Char = '\237' %(printable_237)%;
'�' : Char = '\238' %(printable_238)%;
'�' : Char = '\239' %(printable_239)%;
'�' : Char = '\240' %(printable_240)%;
'�' : Char = '\241' %(printable_241)%;
'�' : Char = '\242' %(printable_242)%;
'�' : Char = '\243' %(printable_243)%;
'�' : Char = '\244' %(printable_244)%;
'�' : Char = '\245' %(printable_245)%;
'�' : Char = '\246' %(printable_246)%;
'�' : Char = '\247' %(printable_247)%;
'�' : Char = '\248' %(printable_248)%;
'�' : Char = '\249' %(printable_249)%;
'�' : Char = '\250' %(printable_250)%;
'�' : Char = '\251' %(printable_251)%;
'�' : Char = '\252' %(printable_252)%;
'�' : Char = '\253' %(printable_253)%;
'�' : Char = '\254' %(printable_254)%;
'�' : Char = '\255' %(printable_255)%
predfun isLetter(c : Char) :? Unit = ((ord ('A') <= ord (c) /\ ord
\/ (ord ('a') <= ord (c) /\ ord (c) <= ord ('z')))
isDigit(c : Char) :? Unit = ord ('0') <= ord (c) /\ ord (c) <= ord
isPrintable(c : Char) :? Unit = ((ord (' ') <= ord (c) /\ ord (c)
\/ (ord (' ') <= ord (c) /\ ord (c) <= ord ('�')))
%% alternative definition of characters as '\o ppp',
%% where p in {0,1,...,7} :
op '\o000' : Char = '\000' %(slash_o000)%;
'\o001' : Char = '\001' %(slash_o001)%;
'\o002' : Char = '\002' %(slash_o002)%;
'\o003' : Char = '\003' %(slash_o003)%;
'\o004' : Char = '\004' %(slash_o004)%;
'\o005' : Char = '\005' %(slash_o005)%;
'\o006' : Char = '\006' %(slash_o006)%;
'\o007' : Char = '\007' %(slash_o007)%;
'\o010' : Char = '\008' %(slash_o010)%;
'\o011' : Char = '\009' %(slash_o011)%;
'\o012' : Char = '\010' %(slash_o012)%;
'\o013' : Char = '\011' %(slash_o013)%;
'\o014' : Char = '\012' %(slash_o014)%;
'\o015' : Char = '\013' %(slash_o015)%;
'\o016' : Char = '\014' %(slash_o016)%;
'\o017' : Char = '\015' %(slash_o017)%;
'\o020' : Char = '\016' %(slash_o020)%;
'\o021' : Char = '\017' %(slash_o021)%;
'\o022' : Char = '\018' %(slash_o022)%;
'\o023' : Char = '\019' %(slash_o023)%;
'\o024' : Char = '\020' %(slash_o024)%;
'\o025' : Char = '\021' %(slash_o025)%;
'\o026' : Char = '\022' %(slash_o026)%;
'\o027' : Char = '\023' %(slash_o027)%;
'\o030' : Char = '\024' %(slash_o030)%;
'\o031' : Char = '\025' %(slash_o031)%;
'\o032' : Char = '\026' %(slash_o032)%;
'\o033' : Char = '\027' %(slash_o033)%;
'\o034' : Char = '\028' %(slash_o034)%;
'\o035' : Char = '\029' %(slash_o035)%;
'\o036' : Char = '\030' %(slash_o036)%;
'\o037' : Char = '\031' %(slash_o037)%;
'\o040' : Char = '\032' %(slash_o040)%;
'\o041' : Char = '\033' %(slash_o041)%;
'\o042' : Char = '\034' %(slash_o042)%;
'\o043' : Char = '\035' %(slash_o043)%;
'\o044' : Char = '\036' %(slash_o044)%;
'\o045' : Char = '\037' %(slash_o045)%;
'\o046' : Char = '\038' %(slash_o046)%;
'\o047' : Char = '\039' %(slash_o047)%;
'\o050' : Char = '\040' %(slash_o050)%;
'\o051' : Char = '\041' %(slash_o051)%;
'\o052' : Char = '\042' %(slash_o052)%;
'\o053' : Char = '\043' %(slash_o053)%;
'\o054' : Char = '\044' %(slash_o054)%;
'\o055' : Char = '\045' %(slash_o055)%;
'\o056' : Char = '\046' %(slash_o056)%;
'\o057' : Char = '\047' %(slash_o057)%;
'\o060' : Char = '\048' %(slash_o060)%;
'\o061' : Char = '\049' %(slash_o061)%;
'\o062' : Char = '\050' %(slash_o062)%;
'\o063' : Char = '\051' %(slash_o063)%;
'\o064' : Char = '\052' %(slash_o064)%;
'\o065' : Char = '\053' %(slash_o065)%;
'\o066' : Char = '\054' %(slash_o066)%;
'\o067' : Char = '\055' %(slash_o067)%;
'\o070' : Char = '\056' %(slash_o070)%;
'\o071' : Char = '\057' %(slash_o071)%;
'\o072' : Char = '\058' %(slash_o072)%;
'\o073' : Char = '\059' %(slash_o073)%;
'\o074' : Char = '\060' %(slash_o074)%;
'\o075' : Char = '\061' %(slash_o075)%;
'\o076' : Char = '\062' %(slash_o076)%;
'\o077' : Char = '\063' %(slash_o077)%;
'\o100' : Char = '\064' %(slash_o100)%;
'\o101' : Char = '\065' %(slash_o101)%;
'\o102' : Char = '\066' %(slash_o102)%;
'\o103' : Char = '\067' %(slash_o103)%;
'\o104' : Char = '\068' %(slash_o104)%;
'\o105' : Char = '\069' %(slash_o105)%;
'\o106' : Char = '\070' %(slash_o106)%;
'\o107' : Char = '\071' %(slash_o107)%;
'\o110' : Char = '\072' %(slash_o110)%;
'\o111' : Char = '\073' %(slash_o111)%;
'\o112' : Char = '\074' %(slash_o112)%;
'\o113' : Char = '\075' %(slash_o113)%;
'\o114' : Char = '\076' %(slash_o114)%;
'\o115' : Char = '\077' %(slash_o115)%;
'\o116' : Char = '\078' %(slash_o116)%;
'\o117' : Char = '\079' %(slash_o117)%;
'\o120' : Char = '\080' %(slash_o120)%;
'\o121' : Char = '\081' %(slash_o121)%;
'\o122' : Char = '\082' %(slash_o122)%;
'\o123' : Char = '\083' %(slash_o123)%;
'\o124' : Char = '\084' %(slash_o124)%;
'\o125' : Char = '\085' %(slash_o125)%;
'\o126' : Char = '\086' %(slash_o126)%;
'\o127' : Char = '\087' %(slash_o127)%;
'\o130' : Char = '\088' %(slash_o130)%;
'\o131' : Char = '\089' %(slash_o131)%;
'\o132' : Char = '\090' %(slash_o132)%;
'\o133' : Char = '\091' %(slash_o133)%;
'\o134' : Char = '\092' %(slash_o134)%;
'\o135' : Char = '\093' %(slash_o135)%;
'\o136' : Char = '\094' %(slash_o136)%;
'\o137' : Char = '\095' %(slash_o137)%;
'\o140' : Char = '\096' %(slash_o140)%;
'\o141' : Char = '\097' %(slash_o141)%;
'\o142' : Char = '\098' %(slash_o142)%;
'\o143' : Char = '\099' %(slash_o143)%;
'\o144' : Char = '\100' %(slash_o144)%;
'\o145' : Char = '\101' %(slash_o145)%;
'\o146' : Char = '\102' %(slash_o146)%;
'\o147' : Char = '\103' %(slash_o147)%;
'\o150' : Char = '\104' %(slash_o150)%;
'\o151' : Char = '\105' %(slash_o151)%;
'\o152' : Char = '\106' %(slash_o152)%;
'\o153' : Char = '\107' %(slash_o153)%;
'\o154' : Char = '\108' %(slash_o154)%;
'\o155' : Char = '\109' %(slash_o155)%;
'\o156' : Char = '\110' %(slash_o156)%;
'\o157' : Char = '\111' %(slash_o157)%;
'\o160' : Char = '\112' %(slash_o160)%;
'\o161' : Char = '\113' %(slash_o161)%;
'\o162' : Char = '\114' %(slash_o162)%;
'\o163' : Char = '\115' %(slash_o163)%;
'\o164' : Char = '\116' %(slash_o164)%;
'\o165' : Char = '\117' %(slash_o165)%;
'\o166' : Char = '\118' %(slash_o166)%;
'\o167' : Char = '\119' %(slash_o167)%;
'\o170' : Char = '\120' %(slash_o170)%;
'\o171' : Char = '\121' %(slash_o171)%;
'\o172' : Char = '\122' %(slash_o172)%;
'\o173' : Char = '\123' %(slash_o173)%;
'\o174' : Char = '\124' %(slash_o174)%;
'\o175' : Char = '\125' %(slash_o175)%;
'\o176' : Char = '\126' %(slash_o176)%;
'\o177' : Char = '\127' %(slash_o177)%;
'\o200' : Char = '\128' %(slash_o200)%;
'\o201' : Char = '\129' %(slash_o201)%;
'\o202' : Char = '\130' %(slash_o202)%;
'\o203' : Char = '\131' %(slash_o203)%;
'\o204' : Char = '\132' %(slash_o204)%;
'\o205' : Char = '\133' %(slash_o205)%;
'\o206' : Char = '\134' %(slash_o206)%;
'\o207' : Char = '\135' %(slash_o207)%;
'\o210' : Char = '\136' %(slash_o210)%;
'\o211' : Char = '\137' %(slash_o211)%;
'\o212' : Char = '\138' %(slash_o212)%;
'\o213' : Char = '\139' %(slash_o213)%;
'\o214' : Char = '\140' %(slash_o214)%;
'\o215' : Char = '\141' %(slash_o215)%;
'\o216' : Char = '\142' %(slash_o216)%;
'\o217' : Char = '\143' %(slash_o217)%;
'\o220' : Char = '\144' %(slash_o220)%;
'\o221' : Char = '\145' %(slash_o221)%;
'\o222' : Char = '\146' %(slash_o222)%;
'\o223' : Char = '\147' %(slash_o223)%;
'\o224' : Char = '\148' %(slash_o224)%;
'\o225' : Char = '\149' %(slash_o225)%;
'\o226' : Char = '\150' %(slash_o226)%;
'\o227' : Char = '\151' %(slash_o227)%;
'\o230' : Char = '\152' %(slash_o230)%;
'\o231' : Char = '\153' %(slash_o231)%;
'\o232' : Char = '\154' %(slash_o232)%;
'\o233' : Char = '\155' %(slash_o233)%;
'\o234' : Char = '\156' %(slash_o234)%;
'\o235' : Char = '\157' %(slash_o235)%;
'\o236' : Char = '\158' %(slash_o236)%;
'\o237' : Char = '\159' %(slash_o237)%;
'\o240' : Char = '\160' %(slash_o240)%;
'\o241' : Char = '\161' %(slash_o241)%;
'\o242' : Char = '\162' %(slash_o242)%;
'\o243' : Char = '\163' %(slash_o243)%;
'\o244' : Char = '\164' %(slash_o244)%;
'\o245' : Char = '\165' %(slash_o245)%;
'\o246' : Char = '\166' %(slash_o246)%;
'\o247' : Char = '\167' %(slash_o247)%;
'\o250' : Char = '\168' %(slash_o250)%;
'\o251' : Char = '\169' %(slash_o251)%;
'\o252' : Char = '\170' %(slash_o252)%;
'\o253' : Char = '\171' %(slash_o253)%;
'\o254' : Char = '\172' %(slash_o254)%;
'\o255' : Char = '\173' %(slash_o255)%;
'\o256' : Char = '\174' %(slash_o256)%;
'\o257' : Char = '\175' %(slash_o257)%;
'\o260' : Char = '\176' %(slash_o260)%;
'\o261' : Char = '\177' %(slash_o261)%;
'\o262' : Char = '\178' %(slash_o262)%;
'\o263' : Char = '\179' %(slash_o263)%;
'\o264' : Char = '\180' %(slash_o264)%;
'\o265' : Char = '\181' %(slash_o265)%;
'\o266' : Char = '\182' %(slash_o266)%;
'\o267' : Char = '\183' %(slash_o267)%;
'\o270' : Char = '\184' %(slash_o270)%;
'\o271' : Char = '\185' %(slash_o271)%;
'\o272' : Char = '\186' %(slash_o272)%;
'\o273' : Char = '\187' %(slash_o273)%;
'\o274' : Char = '\188' %(slash_o274)%;
'\o275' : Char = '\189' %(slash_o275)%;
'\o276' : Char = '\190' %(slash_o276)%;
'\o277' : Char = '\191' %(slash_o277)%;
'\o300' : Char = '\192' %(slash_o300)%;
'\o301' : Char = '\193' %(slash_o301)%;
'\o302' : Char = '\194' %(slash_o302)%;
'\o303' : Char = '\195' %(slash_o303)%;
'\o304' : Char = '\196' %(slash_o304)%;
'\o305' : Char = '\197' %(slash_o305)%;
'\o306' : Char = '\198' %(slash_o306)%;
'\o307' : Char = '\199' %(slash_o307)%;
'\o310' : Char = '\200' %(slash_o310)%;
'\o311' : Char = '\201' %(slash_o311)%;
'\o312' : Char = '\202' %(slash_o312)%;
'\o313' : Char = '\203' %(slash_o313)%;
'\o314' : Char = '\204' %(slash_o314)%;
'\o315' : Char = '\205' %(slash_o315)%;
'\o316' : Char = '\206' %(slash_o316)%;
'\o317' : Char = '\207' %(slash_o317)%;
'\o320' : Char = '\208' %(slash_o320)%;
'\o321' : Char = '\209' %(slash_o321)%;
'\o322' : Char = '\210' %(slash_o322)%;
'\o323' : Char = '\211' %(slash_o323)%;
'\o324' : Char = '\212' %(slash_o324)%;
'\o325' : Char = '\213' %(slash_o325)%;
'\o326' : Char = '\214' %(slash_o326)%;
'\o327' : Char = '\215' %(slash_o327)%;
'\o330' : Char = '\216' %(slash_o330)%;
'\o331' : Char = '\217' %(slash_o331)%;
'\o332' : Char = '\218' %(slash_o332)%;
'\o333' : Char = '\219' %(slash_o333)%;
'\o334' : Char = '\220' %(slash_o334)%;
'\o335' : Char = '\221' %(slash_o335)%;
'\o336' : Char = '\222' %(slash_o336)%;
'\o337' : Char = '\223' %(slash_o337)%;
'\o340' : Char = '\224' %(slash_o340)%;
'\o341' : Char = '\225' %(slash_o341)%;
'\o342' : Char = '\226' %(slash_o342)%;
'\o343' : Char = '\227' %(slash_o343)%;
'\o344' : Char = '\228' %(slash_o344)%;
'\o345' : Char = '\229' %(slash_o345)%;
'\o346' : Char = '\230' %(slash_o346)%;
'\o347' : Char = '\231' %(slash_o347)%;
'\o350' : Char = '\232' %(slash_o350)%;
'\o351' : Char = '\233' %(slash_o351)%;
'\o352' : Char = '\234' %(slash_o352)%;
'\o353' : Char = '\235' %(slash_o353)%;
'\o354' : Char = '\236' %(slash_o354)%;
'\o355' : Char = '\237' %(slash_o355)%;
'\o356' : Char = '\238' %(slash_o356)%;
'\o357' : Char = '\239' %(slash_o357)%;
'\o360' : Char = '\240' %(slash_o360)%;
'\o361' : Char = '\241' %(slash_o361)%;
'\o362' : Char = '\242' %(slash_o362)%;
'\o363' : Char = '\243' %(slash_o363)%;
'\o364' : Char = '\244' %(slash_o364)%;
'\o365' : Char = '\245' %(slash_o365)%;
'\o366' : Char = '\246' %(slash_o366)%;
'\o367' : Char = '\247' %(slash_o367)%;
'\o370' : Char = '\248' %(slash_o370)%;
'\o371' : Char = '\249' %(slash_o371)%;
'\o372' : Char = '\250' %(slash_o372)%;
'\o373' : Char = '\251' %(slash_o373)%;
'\o374' : Char = '\252' %(slash_o374)%;
'\o375' : Char = '\253' %(slash_o375)%;
'\o376' : Char = '\254' %(slash_o376)%;
'\o377' : Char = '\255' %(slash_o377)%
%% alternative definition of characters as '\xhh',
%% where h in {0,1,..., F} :
op '\x00' : Char = '\000' %(slash_x00)%;
'\x01' : Char = '\001' %(slash_x01)%;
'\x02' : Char = '\002' %(slash_x02)%;
'\x03' : Char = '\003' %(slash_x03)%;
'\x04' : Char = '\004' %(slash_x04)%;
'\x05' : Char = '\005' %(slash_x05)%;
'\x06' : Char = '\006' %(slash_x06)%;
'\x07' : Char = '\007' %(slash_x07)%;
'\x08' : Char = '\008' %(slash_x08)%;
'\x09' : Char = '\009' %(slash_x09)%;
'\x0A' : Char = '\010' %(slash_x0A)%;
'\x0B' : Char = '\011' %(slash_x0B)%;
'\x0C' : Char = '\012' %(slash_x0C)%;
'\x0D' : Char = '\013' %(slash_x0D)%;
'\x0E' : Char = '\014' %(slash_x0E)%;
'\x0F' : Char = '\015' %(slash_x0F)%;
'\x10' : Char = '\016' %(slash_x10)%;
'\x11' : Char = '\017' %(slash_x11)%;
'\x12' : Char = '\018' %(slash_x12)%;
'\x13' : Char = '\019' %(slash_x13)%;
'\x14' : Char = '\020' %(slash_x14)%;
'\x15' : Char = '\021' %(slash_x15)%;
'\x16' : Char = '\022' %(slash_x16)%;
'\x17' : Char = '\023' %(slash_x17)%;
'\x18' : Char = '\024' %(slash_x18)%;
'\x19' : Char = '\025' %(slash_x19)%;
'\x1A' : Char = '\026' %(slash_x1A)%;
'\x1B' : Char = '\027' %(slash_x1B)%;
'\x1C' : Char = '\028' %(slash_x1C)%;
'\x1D' : Char = '\029' %(slash_x1D)%;
'\x1E' : Char = '\030' %(slash_x1E)%;
'\x1F' : Char = '\031' %(slash_x1F)%;
'\x20' : Char = '\032' %(slash_x20)%;
'\x21' : Char = '\033' %(slash_x21)%;
'\x22' : Char = '\034' %(slash_x22)%;
'\x23' : Char = '\035' %(slash_x23)%;
'\x24' : Char = '\036' %(slash_x24)%;
'\x25' : Char = '\037' %(slash_x25)%;
'\x26' : Char = '\038' %(slash_x26)%;
'\x27' : Char = '\039' %(slash_x27)%;
'\x28' : Char = '\040' %(slash_x28)%;
'\x29' : Char = '\041' %(slash_x29)%;
'\x2A' : Char = '\042' %(slash_x2A)%;
'\x2B' : Char = '\043' %(slash_x2B)%;
'\x2C' : Char = '\044' %(slash_x2C)%;
'\x2D' : Char = '\045' %(slash_x2D)%;
'\x2E' : Char = '\046' %(slash_x2E)%;
'\x2F' : Char = '\047' %(slash_x2F)%;
'\x30' : Char = '\048' %(slash_x30)%;
'\x31' : Char = '\049' %(slash_x31)%;
'\x32' : Char = '\050' %(slash_x32)%;
'\x33' : Char = '\051' %(slash_x33)%;
'\x34' : Char = '\052' %(slash_x34)%;
'\x35' : Char = '\053' %(slash_x35)%;
'\x36' : Char = '\054' %(slash_x36)%;
'\x37' : Char = '\055' %(slash_x37)%;
'\x38' : Char = '\056' %(slash_x38)%;
'\x39' : Char = '\057' %(slash_x39)%;
'\x3A' : Char = '\058' %(slash_x3A)%;
'\x3B' : Char = '\059' %(slash_x3B)%;
'\x3C' : Char = '\060' %(slash_x3C)%;
'\x3D' : Char = '\061' %(slash_x3D)%;
'\x3E' : Char = '\062' %(slash_x3E)%;
'\x3F' : Char = '\063' %(slash_x3F)%;
'\x40' : Char = '\064' %(slash_x40)%;
'\x41' : Char = '\065' %(slash_x41)%;
'\x42' : Char = '\066' %(slash_x42)%;
'\x43' : Char = '\067' %(slash_x43)%;
'\x44' : Char = '\068' %(slash_x44)%;
'\x45' : Char = '\069' %(slash_x45)%;
'\x46' : Char = '\070' %(slash_x46)%;
'\x47' : Char = '\071' %(slash_x47)%;
'\x48' : Char = '\072' %(slash_x48)%;
'\x49' : Char = '\073' %(slash_x49)%;
'\x4A' : Char = '\074' %(slash_x4A)%;
'\x4B' : Char = '\075' %(slash_x4B)%;
'\x4C' : Char = '\076' %(slash_x4C)%;
'\x4D' : Char = '\077' %(slash_x4D)%;
'\x4E' : Char = '\078' %(slash_x4E)%;
'\x4F' : Char = '\079' %(slash_x4F)%;
'\x50' : Char = '\080' %(slash_x50)%;
'\x51' : Char = '\081' %(slash_x51)%;
'\x52' : Char = '\082' %(slash_x52)%;
'\x53' : Char = '\083' %(slash_x53)%;
'\x54' : Char = '\084' %(slash_x54)%;
'\x55' : Char = '\085' %(slash_x55)%;
'\x56' : Char = '\086' %(slash_x56)%;
'\x57' : Char = '\087' %(slash_x57)%;
'\x58' : Char = '\088' %(slash_x58)%;
'\x59' : Char = '\089' %(slash_x59)%;
'\x5A' : Char = '\090' %(slash_x5A)%;
'\x5B' : Char = '\091' %(slash_x5B)%;
'\x5C' : Char = '\092' %(slash_x5C)%;
'\x5D' : Char = '\093' %(slash_x5D)%;
'\x5E' : Char = '\094' %(slash_x5E)%;
'\x5F' : Char = '\095' %(slash_x5F)%;
'\x60' : Char = '\096' %(slash_x60)%;
'\x61' : Char = '\097' %(slash_x61)%;
'\x62' : Char = '\098' %(slash_x62)%;
'\x63' : Char = '\099' %(slash_x63)%;
'\x64' : Char = '\100' %(slash_x64)%;
'\x65' : Char = '\101' %(slash_x65)%;
'\x66' : Char = '\102' %(slash_x66)%;
'\x67' : Char = '\103' %(slash_x67)%;
'\x68' : Char = '\104' %(slash_x68)%;
'\x69' : Char = '\105' %(slash_x69)%;
'\x6A' : Char = '\106' %(slash_x6A)%;
'\x6B' : Char = '\107' %(slash_x6B)%;
'\x6C' : Char = '\108' %(slash_x6C)%;
'\x6D' : Char = '\109' %(slash_x6D)%;
'\x6E' : Char = '\110' %(slash_x6E)%;
'\x6F' : Char = '\111' %(slash_x6F)%;
'\x70' : Char = '\112' %(slash_x70)%;
'\x71' : Char = '\113' %(slash_x71)%;
'\x72' : Char = '\114' %(slash_x72)%;
'\x73' : Char = '\115' %(slash_x73)%;
'\x74' : Char = '\116' %(slash_x74)%;
'\x75' : Char = '\117' %(slash_x75)%;
'\x76' : Char = '\118' %(slash_x76)%;
'\x77' : Char = '\119' %(slash_x77)%;
'\x78' : Char = '\120' %(slash_x78)%;
'\x79' : Char = '\121' %(slash_x79)%;
'\x7A' : Char = '\122' %(slash_x7A)%;
'\x7B' : Char = '\123' %(slash_x7B)%;
'\x7C' : Char = '\124' %(slash_x7C)%;
'\x7D' : Char = '\125' %(slash_x7D)%;
'\x7E' : Char = '\126' %(slash_x7E)%;
'\x7F' : Char = '\127' %(slash_x7F)%;
'\x80' : Char = '\128' %(slash_x80)%;
'\x81' : Char = '\129' %(slash_x81)%;
'\x82' : Char = '\130' %(slash_x82)%;
'\x83' : Char = '\131' %(slash_x83)%;
'\x84' : Char = '\132' %(slash_x84)%;
'\x85' : Char = '\133' %(slash_x85)%;
'\x86' : Char = '\134' %(slash_x86)%;
'\x87' : Char = '\135' %(slash_x87)%;
'\x88' : Char = '\136' %(slash_x88)%;
'\x89' : Char = '\137' %(slash_x89)%;
'\x8A' : Char = '\138' %(slash_x8A)%;
'\x8B' : Char = '\139' %(slash_x8B)%;
'\x8C' : Char = '\140' %(slash_x8C)%;
'\x8D' : Char = '\141' %(slash_x8D)%;
'\x8E' : Char = '\142' %(slash_x8E)%;
'\x8F' : Char = '\143' %(slash_x8F)%;
'\x90' : Char = '\144' %(slash_x90)%;
'\x91' : Char = '\145' %(slash_x91)%;
'\x92' : Char = '\146' %(slash_x92)%;
'\x93' : Char = '\147' %(slash_x93)%;
'\x94' : Char = '\148' %(slash_x94)%;
'\x95' : Char = '\149' %(slash_x95)%;
'\x96' : Char = '\150' %(slash_x96)%;
'\x97' : Char = '\151' %(slash_x97)%;
'\x98' : Char = '\152' %(slash_x98)%;
'\x99' : Char = '\153' %(slash_x99)%;
'\x9A' : Char = '\154' %(slash_x9A)%;
'\x9B' : Char = '\155' %(slash_x9B)%;
'\x9C' : Char = '\156' %(slash_x9C)%;
'\x9D' : Char = '\157' %(slash_x9D)%;
'\x9E' : Char = '\158' %(slash_x9E)%;
'\x9F' : Char = '\159' %(slash_x9F)%;
'\xA0' : Char = '\160' %(slash_xA0)%;
'\xA1' : Char = '\161' %(slash_xA1)%;
'\xA2' : Char = '\162' %(slash_xA2)%;
'\xA3' : Char = '\163' %(slash_xA3)%;
'\xA4' : Char = '\164' %(slash_xA4)%;
'\xA5' : Char = '\165' %(slash_xA5)%;
'\xA6' : Char = '\166' %(slash_xA6)%;
'\xA7' : Char = '\167' %(slash_xA7)%;
'\xA8' : Char = '\168' %(slash_xA8)%;
'\xA9' : Char = '\169' %(slash_xA9)%;
'\xAA' : Char = '\170' %(slash_xAA)%;
'\xAB' : Char = '\171' %(slash_xAB)%;
'\xAC' : Char = '\172' %(slash_xAC)%;
'\xAD' : Char = '\173' %(slash_xAD)%;
'\xAE' : Char = '\174' %(slash_xAE)%;
'\xAF' : Char = '\175' %(slash_xAF)%;
'\xB0' : Char = '\176' %(slash_xB0)%;
'\xB1' : Char = '\177' %(slash_xB1)%;
'\xB2' : Char = '\178' %(slash_xB2)%;
'\xB3' : Char = '\179' %(slash_xB3)%;
'\xB4' : Char = '\180' %(slash_xB4)%;
'\xB5' : Char = '\181' %(slash_xB5)%;
'\xB6' : Char = '\182' %(slash_xB6)%;
'\xB7' : Char = '\183' %(slash_xB7)%;
'\xB8' : Char = '\184' %(slash_xB8)%;
'\xB9' : Char = '\185' %(slash_xB9)%;
'\xBA' : Char = '\186' %(slash_xBA)%;
'\xBB' : Char = '\187' %(slash_xBB)%;
'\xBC' : Char = '\188' %(slash_xBC)%;
'\xBD' : Char = '\189' %(slash_xBD)%;
'\xBE' : Char = '\190' %(slash_xBE)%;
'\xBF' : Char = '\191' %(slash_xBF)%;
'\xC0' : Char = '\192' %(slash_xC0)%;
'\xC1' : Char = '\193' %(slash_xC1)%;
'\xC2' : Char = '\194' %(slash_xC2)%;
'\xC3' : Char = '\195' %(slash_xC3)%;
'\xC4' : Char = '\196' %(slash_xC4)%;
'\xC5' : Char = '\197' %(slash_xC5)%;
'\xC6' : Char = '\198' %(slash_xC6)%;
'\xC7' : Char = '\199' %(slash_xC7)%;
'\xC8' : Char = '\200' %(slash_xC8)%;
'\xC9' : Char = '\201' %(slash_xC9)%;
'\xCA' : Char = '\202' %(slash_xCA)%;
'\xCB' : Char = '\203' %(slash_xCB)%;
'\xCC' : Char = '\204' %(slash_xCC)%;
'\xCD' : Char = '\205' %(slash_xCD)%;
'\xCE' : Char = '\206' %(slash_xCE)%;
'\xCF' : Char = '\207' %(slash_xCF)%;
'\xD0' : Char = '\208' %(slash_xD0)%;
'\xD1' : Char = '\209' %(slash_xD1)%;
'\xD2' : Char = '\210' %(slash_xD2)%;
'\xD3' : Char = '\211' %(slash_xD3)%;
'\xD4' : Char = '\212' %(slash_xD4)%;
'\xD5' : Char = '\213' %(slash_xD5)%;
'\xD6' : Char = '\214' %(slash_xD6)%;
'\xD7' : Char = '\215' %(slash_xD7)%;
'\xD8' : Char = '\216' %(slash_xD8)%;
'\xD9' : Char = '\217' %(slash_xD9)%;
'\xDA' : Char = '\218' %(slash_xDA)%;
'\xDB' : Char = '\219' %(slash_xDB)%;
'\xDC' : Char = '\220' %(slash_xDC)%;
'\xDD' : Char = '\221' %(slash_xDD)%;
'\xDE' : Char = '\222' %(slash_xDE)%;
'\xDF' : Char = '\223' %(slash_xDF)%;
'\xE0' : Char = '\224' %(slash_xE0)%;
'\xE1' : Char = '\225' %(slash_xE1)%;
'\xE2' : Char = '\226' %(slash_xE2)%;
'\xE3' : Char = '\227' %(slash_xE3)%;
'\xE4' : Char = '\228' %(slash_xE4)%;
'\xE5' : Char = '\229' %(slash_xE5)%;
'\xE6' : Char = '\230' %(slash_xE6)%;
'\xE7' : Char = '\231' %(slash_xE7)%;
'\xE8' : Char = '\232' %(slash_xE8)%;
'\xE9' : Char = '\233' %(slash_xE9)%;
'\xEA' : Char = '\234' %(slash_xEA)%;
'\xEB' : Char = '\235' %(slash_xEB)%;
'\xEC' : Char = '\236' %(slash_xEC)%;
'\xED' : Char = '\237' %(slash_xED)%;
'\xEE' : Char = '\238' %(slash_xEE)%;
'\xEF' : Char = '\239' %(slash_xEF)%;
'\xF0' : Char = '\240' %(slash_xF0)%;
'\xF1' : Char = '\241' %(slash_xF1)%;
'\xF2' : Char = '\242' %(slash_xF2)%;
'\xF3' : Char = '\243' %(slash_xF3)%;
'\xF4' : Char = '\244' %(slash_xF4)%;
'\xF5' : Char = '\245' %(slash_xF5)%;
'\xF6' : Char = '\246' %(slash_xF6)%;
'\xF7' : Char = '\247' %(slash_xF7)%;
'\xF8' : Char = '\248' %(slash_xF8)%;
'\xF9' : Char = '\249' %(slash_xF9)%;
'\xFA' : Char = '\250' %(slash_xFA)%;
'\xFB' : Char = '\251' %(slash_xFB)%;
'\xFC' : Char = '\252' %(slash_xFC)%;
'\xFD' : Char = '\253' %(slash_xFD)%;
'\xFE' : Char = '\254' %(slash_xFE)%;
'\xFF' : Char = '\255' %(slash_xFF)%
op NUL : Char = '\000' %(NUL_def)%;
SOH : Char = '\001' %(SOH_def)%; SYX : Char = '\002' %(SYX_def)%;
ETX : Char = '\003' %(ETX_def)%; EOT : Char = '\004' %(EOT_def)%;
ENQ : Char = '\005' %(ENQ_def)%; ACK : Char = '\006' %(ACK_def)%;
BEL : Char = '\007' %(BEL_def)%; BS : Char = '\008' %(BS_def)%;
HT : Char = '\009' %(HT_def)%; LF : Char = '\010' %(LF_def)%;
VT : Char = '\011' %(VT_def)%; FF : Char = '\012' %(FF_def)%;
CR : Char = '\013' %(CR_def)%; SO : Char = '\014' %(SO_def)%;
SI : Char = '\015' %(SI_def)%; DLE : Char = '\016' %(DLE_def)%;
DC1 : Char = '\017' %(DC1_def)%; DC2 : Char = '\018' %(DC2_def)%;
DC3 : Char = '\019' %(DC3_def)%; DC4 : Char = '\020' %(DC4_def)%;
NAK : Char = '\021' %(NAK_def)%; SYN : Char = '\022' %(SYN_def)%;
ETB : Char = '\023' %(ETB_def)%; CAN : Char = '\024' %(CAN_def)%;
EM : Char = '\025' %(EM_def)%; SUB : Char = '\026' %(SUB_def)%;
ESC : Char = '\027' %(ESC_def)%; FS : Char = '\028' %(FS_def)%;
GS : Char = '\029' %(GS_def)%; RS : Char = '\030' %(RS_def)%;
US : Char = '\031' %(US_def)%; SP : Char = '\032' %(SP_def)%;
DEL : Char = '\127' %(DEL_def)%
%% alternative names for special charcters:
op NL : Char = LF %(NL_def)%; NP : Char = FF %(NP_def)%
op '\n' : Char = NL %(slash_n)%; '\t' : Char = HT %(slash_t)%;
'\v' : Char = VT %(slash_v)%; '\b' : Char = BS %(slash_b)%;
'\r' : Char = CR %(slash_r)%; '\f' : Char = FF %(slash_f)%;
'\a' : Char = BEL %(slash_a)%; '\?' : Char = '?' %(slash_quest)%
op __||__ : a � a -> a,assoc