| changeset 46840 | 42e32c777581 |
| parent 46839 | f7232c078fa5 |
| child 47199 | 15ede9f1da3f |
| 46839:f7232c078fa5 | 46840:42e32c777581 |
|---|---|
1 (* Title: Pure/PIDE/xml.ML |
1 (* Title: Pure/PIDE/xml.ML |
2 Author: David Aspinall |
2 Author: David Aspinall |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer |
4 Author: Makarius |
4 Author: Makarius |
5 |
5 |
6 Untyped XML trees and basic data representation. |
6 Untyped XML trees and representation of ML values. |
7 *) |
7 *) |
8 |
8 |
9 signature XML_DATA_OPS = |
9 signature XML_DATA_OPS = |
10 sig |
10 sig |
11 type 'a A |
11 type 'a A |