| changeset 52546 | 7118524a2a24 |
| parent 52455 | 9a8f4fdac3cf |
| child 54450 | 7815563f50dc |
| 52545:d2ad6eae514f | 52546:7118524a2a24 |
|---|---|
1 (* Title: Pure/pure_syn.ML |
1 (* Title: Pure/pure_syn.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Minimal outer syntax for bootstrapping Pure. |
4 Minimal outer syntax for bootstrapping Isabelle/Pure. |
5 *) |
5 *) |
6 |
6 |
7 structure Pure_Syn: sig end = |
7 structure Pure_Syn: sig end = |
8 struct |
8 struct |
9 |
9 |