| changeset 69446 | 9cf0b79dfb7f |
| parent 69441 | 0bd51c6aaa8b |
| child 75581 | 29654a8e9374 |
| 69445:bff0011cdf42 | 69446:9cf0b79dfb7f |
|---|---|
1 (* Title: Pure/General/bytes.ML |
1 (* Title: Pure/General/bytes.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Immutable byte vectors as ML strings. |
4 Byte-vector messages. |
5 *) |
5 *) |
6 |
6 |
7 signature BYTES = |
7 signature BYTES = |
8 sig |
8 sig |
9 val read_line: BinIO.instream -> string option |
9 val read_line: BinIO.instream -> string option |