| changeset 22665 | cf152ff55d16 |
| parent 22552 | 70f5cf8a0fad |
| child 22799 | ed7d53db2170 |
| 22664:e965391e2864 | 22665:cf152ff55d16 |
|---|---|
1 (* ID: $Id$ |
1 (* ID: $Id$ |
2 Author: Florian Haftmann, TU Muenchen |
2 Author: Florian Haftmann, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Monolithic strings for ML *} |
5 header {* Monolithic strings for ML *} |
6 |
6 |
7 theory MLString |
7 theory MLString |
8 imports List |
8 imports List |
9 begin |
9 begin |
10 |
10 |