expanded class interface CHARACTER_CONSTANTS
   --
   -- Platform-independent, universal, character constants.
   -- Intended to be used as ancestor for classes that need these constants.
   --
   --inherit
   --   ANY
   --      redefine Ctrl_a, Ctrl_b, Ctrl_c, Ctrl_d, Ctrl_e, Ctrl_f, Ctrl_g,
   --	 Ch_bs, Ch_tab, Ctrl_j, Ctrl_k, Ctrl_l, Ctrl_m, Ctrl_n,
   --	 Ctrl_o, Ctrl_p, Ctrl_q, Ctrl_r, Ctrl_s, Ctrl_t, Ctrl_u, Ctrl_v,
   --	 Ctrl_w, Ctrl_x, Ctrl_y, Ctrl_z, Ch_del
   --      end

feature(s) from CHARACTER_CONSTANTS
   -- Character names:

   ctrl_a: CHARACTER

   ctrl_b: CHARACTER

   ctrl_c: CHARACTER

   ctrl_d: CHARACTER

   ctrl_e: CHARACTER

   ctrl_f: CHARACTER

   ctrl_g: CHARACTER

   ch_bs: CHARACTER

   ch_tab: CHARACTER

   ctrl_j: CHARACTER

   ctrl_k: CHARACTER

   ctrl_l: CHARACTER

   ctrl_m: CHARACTER

   ctrl_n: CHARACTER

   ctrl_o: CHARACTER

   ctrl_p: CHARACTER

   ctrl_q: CHARACTER

   ctrl_r: CHARACTER

   ctrl_s: CHARACTER

   ctrl_t: CHARACTER

   ctrl_u: CHARACTER

   ctrl_v: CHARACTER

   ctrl_w: CHARACTER

   ctrl_x: CHARACTER

   ctrl_y: CHARACTER

   ctrl_z: CHARACTER

   ch_del: CHARACTER



end of expanded CHARACTER_CONSTANTS