| changeset 261 | 358f325f4db6 |
| parent 258 | 03145998190b |
| child 302 | 0cbd34857b9e |
| 260:5accec94b6df | 261:358f325f4db6 |
|---|---|
49 | "{" => "\\{" |
49 | "{" => "\\{" |
50 | "|" => "\\isacharbar" |
50 | "|" => "\\isacharbar" |
51 | "}" => "\\}" |
51 | "}" => "\\}" |
52 | "$" => "\\isachardollar" |
52 | "$" => "\\isachardollar" |
53 | "!" => "\\isacharbang" |
53 | "!" => "\\isacharbang" |
54 | "\\<dash>" => "-" |
54 | "\<dash>" => "-" |
55 | c => c); |
55 | c => c); |
56 |
56 |
57 fun get_word str = |
57 fun get_word str = |
58 let |
58 let |
59 fun only_letters [] = true |
59 fun only_letters [] = true |