| changeset 51936 | 972c4f42fd52 |
| parent 51928 | a5265222d6e6 |
| parent 51935 | 916c7fe684e3 |
| child 51937 | db22d73e6c3e |
| 51928:a5265222d6e6 | 51936:972c4f42fd52 |
|---|---|
1 (* Title: Pure/ProofGeneral/pgip.ML |
|
2 Author: David Aspinall |
|
3 |
|
4 Prover-side PGIP abstraction. |
|
5 Not too closely tied to Isabelle, to help with reuse/porting. |
|
6 *) |
|
7 |
|
8 signature PGIP = |
|
9 sig |
|
10 include PGIPTYPES |
|
11 include PGIPMARKUP |
|
12 include PGIPINPUT |
|
13 include PGIPOUTPUT |
|
14 end |
|
15 |
|
16 structure Pgip : PGIP = |
|
17 struct |
|
18 open PgipTypes |
|
19 open PgipMarkup |
|
20 open PgipInput |
|
21 open PgipOutput |
|
22 end |