| changeset 11819 | 9283b3c11234 |
| parent 7024 | 44bd3c094fd6 |
| child 12120 | a08c61932501 |
| 11818:9eab353e810b | 11819:9283b3c11234 |
|---|---|
1 (* Title: Pure/Thy/thy_syn.ML |
1 (* Title: Pure/Thy/thy_syn.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4 |
5 |
5 Provide syntax for old-style theory files. |
6 Provide syntax for *old-style* theory files. |
6 *) |
7 *) |
7 |
8 |
8 signature BASIC_THY_SYN = |
9 signature BASIC_THY_SYN = |
9 sig |
10 sig |
10 val delete_tmpfiles: bool ref |
11 val delete_tmpfiles: bool ref |