1signature UnicodeChars = 2sig 3 4 (* Greek letters *) 5 val alpha : string 6 val beta : string 7 val gamma : string 8 val delta : string 9 val zeta : string 10 val eta : string 11 val theta : string 12 val kappa : string 13 val lambda : string 14 val mu : string 15 val nu : string 16 val xi : string 17 val pi : string 18 val rho : string 19 val sigma : string 20 val tau : string 21 val phi : string 22 val psi : string 23 val omega : string 24 25 val Gamma : string 26 val Delta : string 27 val Theta : string 28 val Lambda : string 29 val Xi : string 30 val Sigma : string 31 val Pi : string 32 val Phi : string 33 val Psi : string 34 val Omega : string 35 36 (* superscripts *) 37 val sup_0 : string 38 val sup_1 : string 39 val sup_2 : string 40 val sup_3 : string 41 val sup_4 : string 42 val sup_5 : string 43 val sup_6 : string 44 val sup_7 : string 45 val sup_8 : string 46 val sup_9 : string 47 val sup_lparen : string 48 val sup_rparen : string 49 val sup_eq : string 50 val sup_plus : string 51 val sup_minus : string 52 val sup_h : string 53 val sup_i : string 54 val sup_j : string 55 val sup_l : string 56 val sup_n : string 57 val sup_r : string 58 val sup_s : string 59 val sup_w : string 60 val sup_x : string 61 val sup_y : string 62 val sup_gamma : string 63 64 (* subscripts *) 65 val sub_plus : string 66 val sub_r : string 67 68 (* arrows *) 69 val rightarrow : string 70 val leftarrow : string 71 val longleftarrow : string 72 val longrightarrow : string 73 val Rightarrow : string 74 val Leftarrow : string 75 val longdoublerightarrow : string 76 val longdoubleleftarrow : string 77 val mapsto : string 78 val mapsfrom : string 79 val longmapsto : string 80 val longmapsfrom : string 81 val hookleftarrow : string 82 val hookrightarrow : string 83 84 (* brackets, braces and parentheses *) 85 val double_bracel : string 86 val double_bracer : string 87 val langle : string 88 val rangle : string 89 val double_langle : string 90 val double_rangle : string 91 val lensel : string 92 val lenser : string 93 94 (* stars *) 95 val blackstar : string 96 val whitestar : string 97 val bigasterisk : string 98 val asterisk : string 99 val circlestar : string 100 val stardiaeresis : string 101 102 (* quotation marks *) 103 val ldquo : string 104 val lsquo : string 105 val rdquo : string 106 val rsquo : string 107 108 (* boolTheory connectives *) 109 val forall : string 110 val exists : string 111 val conj : string 112 val disj : string 113 val imp : string 114 val neg : string 115 val neq : string 116 val turnstile : string 117 val iff : string 118 val not_iff : string 119 120 (* arithmeticTheory *) 121 val leq : string 122 val geq : string 123 val minus : string 124 val nats : string 125 val ints : string 126 val rats : string 127 val reals : string 128 129 (* pred_setTheory *) 130 val emptyset : string 131 val union : string 132 val inter : string 133 val subset : string 134 val setelementof : string 135 val not_elementof : string 136 val universal_set : string 137 138 (* other operators *) 139 val doubleplus : string 140 141 (* wordsTheory *) 142 val lo : string 143 val ls : string 144 val hi : string 145 val hs : string 146 val or : string 147 val xor : string 148 val lsl : string 149 val lsr : string 150 val asr : string 151 val rol : string 152 val ror : string 153 154 val isAlpha : string -> bool 155 val isDigit : string -> bool 156 val isAlphaNum : string -> bool 157 val isSymbolic : string -> bool 158 val isMLIdent : string -> bool 159 val isSpace : string -> bool 160 val isSupDigit : string -> bool 161 162 val isAlpha_i : int -> bool 163 val isDigit_i : int -> bool 164 val isAlphaNum_i : int -> bool 165 val isSymbolic_i : int -> bool 166 val isMLIdent_i : int -> bool 167 val isSpace_i : int -> bool 168 val isSupDigit_i : int -> bool 169 170 val supDigitVal : string -> int option 171 val supDigitVal_i : int -> int option 172 173 174end 175