changeset 7114 | f1e787b90fdc |
parent 6227 | 3198f547f8af |
child 7147 | ff492d5d77cc |
7113:ab79d9fa8d8e | 7114:f1e787b90fdc |
---|---|
14 |
14 |
15 structure String = |
15 structure String = |
16 struct |
16 struct |
17 fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) |
17 fun substring (s,i,j) = StringBuiltIns.substring (s, i+1, j) |
18 handle Substring => raise Subscript |
18 handle Substring => raise Subscript |
19 val concat = implode |
|
19 end; |
20 end; |
20 |
21 |
21 |
22 |
22 (** ML system related **) |
23 (** ML system related **) |
23 |
24 |