class Type

var t : Type

class TYPE = Type; TYPE={x.x< t}

type Pred __ :Type- ->Type; Unit :TYPE

class a, b, c

class a, b, c < d; a = b

var s : c

pred tt : s

var x : s

program tt = \ x : s . ()

program __ res __ (x : s; y : t) : s = x;

fst (x : s; y : t) : s = x; snd (x : s; y : t) : t = y

. (\ x : s; y : t . def (x res y)) =

(\ x : s; y : t . (def y) res (def x))

. fst = (__ res __)

pred eq : s � s

. (\ x : s . eq (x, x)) = tt

. (\ x : s; y : s . x res eq (x, y)) =

(\ x : s; y : s . y res eq (x, y))

type s < ? s

program all (p : (? s)) : (? ()) = eq (p, tt)

program And (x, y : (? ())) : (? ()) = t1 () res t2 ()

program __ impl __ (x, y : (? ())) = eq (x, x And y)

program __ or __ (x, y : (? ())) : (? ()) =

all (\ r : (? ()) . ((x impl r) res (y impl r)) impl r);

ex (p : (? s)) : (? ()) =

all (\ r : (? ()) . all (\ x : s . p (x) impl r) impl r);

ff () : (? ()) = all (\ r : (? ()) . r ())

forall x : t; y : t

. %(..)%

x = y

free type Nat ::= 0 |

suc (pre:? Nat)

pred __<=__, __<__, __>=__, __>__ : Nat � Nat; odd, even : Nat

op __+__, __*__ : Nat � Nat -> Nat; __^__ : Nat � Nat -> Nat;

min, max : Nat � Nat -> Nat; +__ : Nat -> Nat; abs : Nat -> Nat;

__! : Nat -> Nat; __-?__ : Nat � Nat ->? Nat;

__/?__ : Nat � Nat ->? Nat;

__div__, __mod__, __quot__, __rem__ : Nat � Nat ->? Nat %()%;

%% Operations to represent natural numbers with digits:

1, 2, 3, 4, 5, 6, 7, 8, 9 : Nat;

__@@__ : Nat � Nat -> Nat

forall m : Nat; n : Nat; r : Nat; s : Nat

. 0 <= n %(Nat_leq_def1)%

. not (suc (n) <= 0) %(Nat_leq_def2)%

. suc (m) <= suc (n) <=> m <= n %(Nat_leq_def3)%

. m >= n <=> n <= m %(Nat_geq_def)%

. m < n <=> (m <= n /\ not (m = n)) %(Nat_less_def)%

. m > n <=> m < n %(Nat_greater_def)%

. 0 + m = m %(Nat_add_0)%

. suc (n) + m = suc (n + m) %(Nat_add_suc)%

. 0 * m = 0 %(Nat_mult_0)%

. suc (n) * m = (n * m) + m %(Nat_mult_suc)%

. m ^ 0 = 1 %(Nat_power_0)%

. m ^ suc (n) = m * m ^ n %(Nat_power_suc)%

. min (m, n) = m when m <= n else n %(Nat_min_def)%

. max (m, n) = n when m <= n else m %(Nat_max_def)%

. + m = m %(plus_def)%

. abs (n) = n %(Nat_abs)%

. odd (m) <=> not even (m) %(Nat_odd_def)%

. even (0) %(Nat_even_0)%

. even (suc (m)) <=> odd (m) %(Nat_even_suc)%

. 0 ! = 1 %(Nat_factorial_0)%

. suc (n) ! = suc (n) * n ! %(Nat_factorial_suc)%

. m -? n = r <=> m = r + n %(Nat_sub_def)%

. not def (m /? 0) %(Nat_divide_0)%

. (m /? n = r <=> m = r * n) if n > 0 %(Nat_divide_Pos)%

. m div n = r <=> (exists s : Nat . m = n * r + s /\ s < n)

%(Nat_div)%

. m mod n = s <=> (exists r : Nat . m = n * r + s /\ s < n)

%(Nat_mod)%

. m quot n = m div n %(Nat_quot)%

. m rem n = m mod n %(Nat_rem)%

. 1 = suc (0) %(Nat_1_def)%

. 2 = suc (1) %(Nat_2_def)%

. 3 = suc (2) %(Nat_3_def)%

. 4 = suc (3) %(Nat_4_def)%

. 5 = suc (4) %(Nat_5_def)%

. 6 = suc (5) %(Nat_6_def)%

. 7 = suc (6) %(Nat_7_def)%

. 8 = suc (7) %(Nat_8_def)%

. 9 = suc (8) %(Nat_9_def)%

. m @@ n = (m * suc (9)) + n %(Nat_decimal_def)%

%% then %def

type Pos = {p : Nat . p > 0}

op 1 : Pos = suc (0) %(Nat_1_as_Pos_def)%;

__*__ : Pos � Pos -> Pos; __+__ : Pos � Nat -> Pos;

__+__ : Nat � Pos -> Pos; suc : Nat -> Pos

%% then %implies

op min, max : Nat � Nat -> Nat,comm, assoc

forall x : Nat; m : Nat; n : Nat; r : Nat; s : Nat; t : Nat;

p : Pos

. def (m -? n) <=> m >= n %(Nat_sub_dom)%

. def (m /? n) <=> m mod n = 0 %(Nat_divide_dom)%

. def (m div n) <=> not (n = 0) %(Nat_div_dom)%

. def (m mod n) <=> not (n = 0) %(Nat_mod_dom)%

. def (m quot n) <=> not (n = 0) %(Nat_quot_dom)%

. def (m rem n) <=> not (n = 0) %(Nat_rem_dom)%

. (r + s) * t = (r * t) + (s * t) %(Nat_distr)%

. max (m, 0) = m %(Nat_max_unit)%

. min (m, 0) = 0 %(Nat_min_0)%

%% end

generated {type Int ::= __-__ (Nat; Nat)}

forall a : Nat; b : Nat; c : Nat; d : Nat

. a - b = c - d <=> a + d = c + b %(Int_equality)%

%% then

type Nat < Int

forall a : Nat

. a = a - 0 %(Int_Nat_embedding)%

pred __<=__, __<__, __>=__, __>__ : Int � Int; odd, even : Int

op 0, 1 : Int; __+__, __-__, __*__ : Int � Int -> Int;

__^__ : Int � Nat -> Int; +__, -__, sign : Int -> Int;

min, max : Int � Int -> Int; abs : Int -> Nat;

__/?__, __div__, __quot__, __rem__ : Int � Int ->? Int;

__mod__ : Int � Int ->? Nat

forall m : Int; n : Int; r : Int; s : Int; a : Nat; b : Nat;

c : Nat; d : Nat

. (a - b) + (c - d) = (a + c) - (b + d) %(Int_add_def)%

. (a - b) * (c - d) = (a * c + b * d) - (b * c + a * d)

%(Int_mult_def)%

. m - n = m + (- n) %(Int_sub_def)%

. + m = m %(Int_pos_def)%

. - (a - b) = b - a %(Int_neg_def)%

. sign (m) = 0 when m = 0 else (1 when m > 0 else - 1)

%(Int_sign_def)%

. m <= n <=> n - m in Nat %(Int_leq_def)%

. m >= n <=> n <= m %(Int_geq_def)%

. m < n <=> (m <= n /\ not (m = n)) %(Int_less_def)%

. m > n <=> m < n %(Int_greater_def)%

. min (m, n) = m when m <= n else n %(Int_min_def)%

. max (m, n) = n when m <= n else m %(Int_max_def)%

. abs (m) = - m if m < 0 %(Int_abs_def)%

. (- 1) ^ a = 1 when even (a) else - 1 %(Int_neg1_power_def)%

. m ^ a = sign (m) ^ a * abs (m) ^ a %(Int_power_def)%

. even (m) <=> even (abs (m)) %(Int_even_def)%

. odd (m) <=> not (even (m)) %(Int_odd_def)%

. m /? n = sign (m) * sign (n) * (abs (m) /? abs (n))

%(Int_divide)%

. m mod n < abs (n) if not n = 0 %(Int_mod_range)%

. m = (m div n) * n + (m mod n) if not n = 0 %(Int_mod__div_def)%

. not def m mod 0 %(Int_mod_zero)%

. not def m div 0 %(Int_div_zero)%

. m quot n = sign (m) * sign (n) * (abs (m) quot abs (n))

%(Int_quot_def)%

. m rem n = sign (m) * sign (n) * (abs (m) rem abs (n))

forall m : Int; n : Int; r : Int; a : Nat; b : Nat . def (a -? b)

=> a -? b = a - b

%(Int_rem_def)%

%% then %implies

%(Int_Nat_sub_compat)%

. m = sign (m) * abs (m) %(Int_abs_decomp)%

. odd (m) <=> odd (abs (m)) %(Int_odd_alt)%

. m /? n = r <=> not n = 0 /\ n * r = n %(Int_divide_dom1)%

. def (m /? n) <=> m mod n = 0 %(Int_divide_dom2)%

. def (m mod n) <=> not n = 0 %(Int_mod_dom)%

. m mod n = m mod abs (n) %(Int_mod_abs)%

. def (m div n) <=> not n = 0 %(Int_div_dom)%

. def (m quot n) <=> not n = 0 %(Int_quot_dom)%

. def (m rem n) <=> not n = 0 %(Int_rem_dom)%

. m = (m quot n) * n + (m rem n) if not n = 0 %(Int_quot_rem)%

%% end

generated {type Rat ::= __/__ (Int; Pos)}

forall i : Int; j : Int; p : Pos; q : Pos

. i / p = j / q <=> i * q = j * p %(Rat_equality)%

type Int < Rat

forall i : Int

. i / 1 = i %(embeddingIntToRat)%

%% then

pred __<=__, __<__, __>=__, __>__ : Rat � Rat

op 0, 1 : Rat; __+__, __-__, __*__ : Rat � Rat -> Rat;

__/__ : Rat � Rat ->? Rat; +__, -__, abs : Rat -> Rat;

__^__ : Rat � Int -> Rat; min, max : Rat � Rat -> Rat

forall p : Pos; q : Pos; n : Nat; i : Int; j : Int; x : Rat;

y : Rat; z : Rat

. (i / p <= j / q <=> i * q <= j * p) %(Rat_leq_def)%

. x >= y <=> y <= x %(Rat_geq_def)%

. x < y <=> (x <= y /\ not (x = y)) %(Rat_less_def)%

. x > y <=> y < x %(Rat_greater_def)%

. (i / p) + (j / q) = (i * q + j * p) / (p * q) %(Rat_add_def)%

. x - y = x + (- y) %(Rat_sub_def)%

. (i / p) * (j / q) = (i * j) / (p * q) %(Rat_mult_def)%

. not def x / 0 %(Rat_divide_def1)%

. (x / y = z <=> z = x * y) if not y = 0 %(Rat_divide_def2)%

. + x = x %(Rat_plus_def)%

. - (i / p) = (- i) / p %(Rat_minus_def)%

. abs (i / p) = abs (i) / p %(Rat_abs_def)%

. x ^ 0 = 1 %(Rat_power_0)%

. x ^ suc (n) = x * x ^ n %(Rat_power_suc)%

. x ^ (- p) = 1 / (x ^ p) %(Rat_power_neg)%

. min (x, y) = x when x <= y else y %(Rat_min_def)%

. max (x, y) = y when x <= y else x

forall i : Int; j : Int; p : Pos; q : Pos . (i / p) - (j / q) =

(i * q - j * p) / (p * q)

%(Rat_max_def)%

%% then %implies

%(Rat_sub_rule)%

. (i / p) / (j / q) = (i / p) * (q / j) if not j = 0

%(Rat_divide_rule)%

pred __<__ : a � a

op __a : b; c : b

type s, t < s

. a = a

var a : t; a : s; b : s

var a : t; a : s; b : s

. a = a

. a = a forall a : t; a : s; b : s . a = a

. a = a

. a = a

. a = a

. a = a

. a = a

type s ::= type s2, s1 |

c |

c (a; a:t; b:t; d:t) |

c (a) ?

free type s ::= type s2, s1 |

c |

c (a; a:t; b:t; d:t) |

c (a) ?

generated {type s ::= type s2, s1 |

c |

c (a; a:t; b:t; d:t) |

c (a) ?}

generated {pred __<__ : a � a; op a : b; c : b; type s, t < s;

type s ::= type s2, s1 |

c |

c (a; a:t; b:t; d:t) |

c (a) ?}

%(sort)%

type %(after-sort)%

s %(bla2)%;

t

%(op)%

op a : b %(bla4)%; c : d %(bla5)%

%(bla6)%

var a : t; a : s; b : s

%(bla8-ignored)%

%(type)%

type t ::= %(c)%

c %(c)% |

e %(e)% |

d %(9)%

%(axiom)%

. a = a %(a1)%

. a = a %(a2)%

%(formula)%

. a = a %(f1)%

. a = a %(f1)%

type s

type s, abcdefghijlklmnopqrstuvwxyz, ABCDEFGHIJKLMONOPQRSTUVWXYZ,

x0123456789,

����������������������������������������������������������, abc,

a_b_c, ab2, ab_2_3_a, a', a'b''2

op __+-*/\&=<>!?:.$@#^~�����������������|__ : s � s -> s

%% NO-BRACKET-SIGNs

op 'a', '\"', '\\', '\n', '\000', '\255', '\x00', '\xFF', '\o000',

'\o377', '^', '1', '2', '3', '4', '5', '6', '7', '8', '9', '0',

'�', '!', '�', '$', '&', '/', '(', ')', '=', '?', '\\' : s

%%characters

op 1, 2, 3, 4 : s; - : s -> s;

__@@__, __exp__, __frac__ : s � s -> s

. def 12

. def 12E34

. def 12E-34

. def 12.34

%%numbers

. def 12.34E34

. def 12.34E+34

. def 12.34E-34

%%fractions

. true %(The true formula)%

. true

%(and this

also goes

along several lines!

and with special stuff: -*/\&=<>BCDEFGHIJKLM!% )%

type s

op __and'__ : s

type a

type a, b, c

type a < b

type a, b, c, d < e

type a = b = c = d = e

type a = {x : b . true}

type s, t

op a : s

op b : s -> s

op c : s � s -> s,assoc, comm, idem, unit a; c : s � s � s -> s

op a : (? s)

op b : s ->? s

op c : s � s ->? s,assoc, comm, idem, unit a

op c : s � s � s ->? s

op a : s = a

op c((x, y : s); z : t) : s = a

op a :? s = a

op c((x, y : s); z : t) :? s = a

type s, t

pred a : ()

pred b : s

pred c : s � s; c : s � s � s

pred c((x, y : s); z : t) <=> false

type Data1 ::= a |

b |

c

type Data2 ::= Cons21 (Data1; Data2) |

Cons22 (Data2; Data1) |

type Data1

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 Data1, Data2, Data3

type Tree ::= Leaf (Data1) |

Forest;

Forest ::= Nil |

Cons (Tree; Forest)

free type List ::= Nil |

Cons (Data1; List)

generated {type Set ::= Mt |

Add (Data1; Set)}

generated {type Set ::= Mt |

Add (Data1; Set)}

generated {type nat; op 0 : nat; succ : nat -> nat}

type s < t

op f, g : s ->? s; g : s -> t;

__+__, __-__, __*__, __/__ : s � s -> s; {} : s; {__} : s -> s

pred p : (); q : s

var x : s; y : s; z : s; r1 : t; r2 : t

. false

var x : s

. true

. 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

p /\ not q (x) /\ q (x)

. not p /\ not q (x) /\ q (x)

if

not p \/ not q (x) \/ q (x)

if

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 f (x)

. f (x) =e= g (x)

. f (x) = g (x)

. r1 in s

. def g (x) : t

. def g (x) as s

. def (op f : s ->? s) (x)

. def (op g : s -> t) (x)

. (op p : () ->? ())

. (op q : s ->? ()) (x)

. def x * y * z + z * y * x

. def {}

. def {x}

. true

forall x : s

. e

forall x : s

. e

free type Boolean ::= True |

False

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)%

type Char

op chr : Nat ->? Char; ord : Char -> Nat

forall n : Nat; c : Char

. 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)%

pred isLetter(c : Char) <=> ((ord ('A') <= ord (c) /\ ord (c) <=

ord ('Z'))

\/ (ord ('a') <= ord (c) /\ ord (c) <= ord ('z')))

%(isLetter_def)%;

isDigit(c : Char) <=> ord ('0') <= ord (c) /\ ord (c) <= ord ('9')

%(isDigit_def)%;

isPrintable(c : Char) <=> ((ord (' ') <= ord (c) /\ ord (c) <= ord

('~'))

\/ (ord (' ') <= ord (c) /\ ord (c) <= ord ('�')))

%(isPrintable_def)%

%% 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)%

%% special characters:

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)%

%% character constants:

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)%