| changeset 21515 | 43d55165b282 |
| parent 21503 | c4ea7e8c3937 |
| child 21858 | 05f57309170c |
| 21514:e7dcae358d1a | 21515:43d55165b282 |
|---|---|
1 (* Title: Pure/General/url.ML |
1 (* Title: Pure/General/url.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
4 |
5 Basic URLs, see RFC 1738. |
5 Basic URLs, see RFC 1738 and RFC 2396. |
6 *) |
6 *) |
7 |
7 |
8 signature URL = |
8 signature URL = |
9 sig |
9 sig |
10 datatype T = |
10 datatype T = |