| changeset 11540 | 23794728cdb7 |
| parent 11519 | 0c96830636a1 |
| child 11543 | d61b913431c5 |
| 11539:0f17da240450 | 11540:23794728cdb7 |
|---|---|
1 (* Title: Pure/proofterm.ML |
1 (* Title: Pure/proofterm.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer |
3 Author: Stefan Berghofer, TU Muenchen |
4 Copyright 2000 TU Muenchen |
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 |
5 |
6 LF style proof terms |
6 LF style proof terms. |
7 *) |
7 *) |
8 |
8 |
9 infix 8 % %% %%%; |
9 infix 8 % %% %%%; |
10 |
10 |
11 signature BASIC_PROOFTERM = |
11 signature BASIC_PROOFTERM = |