| changeset 21637 | a7b156c404e2 |
| child 21641 | d73ab30e82dc |
| 21636:88b815dca68d | 21637:a7b156c404e2 |
|---|---|
1 (* Title: Pure/ProofGeneral/pgip.ML |
|
2 ID: $Id$ |
|
3 Author: David Aspinall |
|
4 |
|
5 Prover-side PGIP abstraction. |
|
6 Not too closely tied to Isabelle, to help with reuse/porting. |
|
7 *) |
|
8 |
|
9 signature PGIP = |
|
10 sig |
|
11 include PGIPTYPES |
|
12 include PGIPINPUT |
|
13 include PGIPOUTPUT |
|
14 end |
|
15 |
|
16 structure Pgip : PGIP = |
|
17 struct |
|
18 open PgipTypes |
|
19 open PgipInput |
|
20 open PgipOutput |
|
21 end |
|
22 |