Lines Matching refs:token
92 fun is_numeral token =
94 val cs = String.explode token
101 (* A <decimal> is a token of the form <numeral>.0*<numeral>. *)
102 fun real_of_decimal token =
104 val (left, right) = Lib.pair_of_list (String.fields (Lib.equal #".") token)
161 ("_", zero_zero (fn token =>
162 if String.isPrefix "#b" token then
164 val binary = String.extract (token, 2, NONE)
170 else if String.isPrefix "#x" token then
172 val hex = String.extract (token, 2, NONE)
256 ("_", zero_zero (fn token =>
257 if is_numeral token then
258 intSyntax.term_of_int (Arbint.fromString token)
286 ("_", zero_zero (fn token =>
287 if is_numeral token then
288 realSyntax.term_of_int (Arbint.fromString token)
318 ("_", zero_zero (fn token =>
319 if is_numeral token then
320 intSyntax.term_of_int (Arbint.fromString token)