Structure UnicodeChars

signature UnicodeChars =
sig

  (* Greek letters *)
  val alpha : string
  val beta : string
  val gamma : string
  val delta : string
  val zeta : string
  val eta : string
  val theta : string
  val kappa : string
  val lambda : string
  val mu : string
  val nu : string
  val xi : string
  val pi : string
  val rho : string
  val sigma : string
  val tau : string
  val phi : string
  val psi : string
  val omega : string

  val Gamma : string
  val Delta : string
  val Theta : string
  val Lambda : string
  val Xi : string
  val Sigma : string
  val Pi : string
  val Phi : string
  val Psi : string
  val Omega : string

  (* superscripts *)
  val sup_0 : string
  val sup_1 : string
  val sup_2 : string
  val sup_3 : string
  val sup_4 : string
  val sup_5 : string
  val sup_6 : string
  val sup_7 : string
  val sup_8 : string
  val sup_9 : string
  val sup_lparen : string
  val sup_rparen : string
  val sup_eq : string
  val sup_plus : string
  val sup_minus : string
  val sup_h : string
  val sup_i : string
  val sup_j : string
  val sup_l : string
  val sup_n : string
  val sup_r : string
  val sup_s : string
  val sup_w : string
  val sup_x : string
  val sup_y : string
  val sup_gamma : string

  (* subscripts *)
  val sub_plus : string
  val sub_r : string

  (* arrows *)
  val rightarrow : string
  val leftarrow : string
  val longleftarrow : string
  val longrightarrow : string
  val Rightarrow : string
  val Leftarrow : string
  val longdoublerightarrow : string
  val longdoubleleftarrow : string
  val mapsto         : string
  val mapsfrom       : string
  val longmapsto     : string
  val longmapsfrom   : string
  val hookleftarrow  : string
  val hookrightarrow : string

  (* brackets, braces and parentheses *)
  val double_bracel : string
  val double_bracer : string
  val langle : string
  val rangle : string
  val double_langle : string
  val double_rangle : string
  val lensel : string
  val lenser : string

  (* stars *)
  val blackstar      : string
  val whitestar      : string
  val bigasterisk    : string
  val asterisk       : string
  val circlestar     : string
  val stardiaeresis  : string

  (* quotation marks *)
  val ldquo : string
  val lsquo : string
  val rdquo : string
  val rsquo : string

  (* boolTheory connectives *)
  val forall : string
  val exists : string
  val conj : string
  val disj : string
  val imp : string
  val neg : string
  val neq : string
  val turnstile : string
  val iff : string
  val not_iff : string

  (* arithmeticTheory *)
  val leq : string
  val geq : string
  val minus : string
  val nats : string
  val ints : string
  val rats : string
  val reals : string

  (* pred_setTheory *)
  val emptyset : string
  val union : string
  val inter : string
  val subset : string
  val setelementof : string
  val not_elementof : string
  val universal_set : string

  (* other operators *)
  val doubleplus : string

  (* wordsTheory *)
  val lo : string
  val ls : string
  val hi : string
  val hs : string
  val or : string
  val xor : string
  val lsl : string
  val lsr : string
  val asr : string
  val rol : string
  val ror : string

  val isAlpha : string -> bool
  val isDigit : string -> bool
  val isAlphaNum : string -> bool
  val isSymbolic : string -> bool
  val isMLIdent : string -> bool
  val isSpace : string -> bool
  val isSupDigit : string -> bool

  val isAlpha_i : int -> bool
  val isDigit_i : int -> bool
  val isAlphaNum_i : int -> bool
  val isSymbolic_i : int -> bool
  val isMLIdent_i : int -> bool
  val isSpace_i : int -> bool
  val isSupDigit_i : int -> bool

  val supDigitVal : string -> int option
  val supDigitVal_i : int -> int option


end

HOL 4, Kananaskis-13