author | wenzelm |
Fri, 18 Jan 2013 16:20:09 +0100 | |
changeset 50974 | 55f8bd61b029 |
parent 29606 | fedb8be05f24 |
permissions | -rw-r--r-- |
21637 | 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 |
|
21641 | 11 |
include PGIPMARKUP |
21637 | 12 |
include PGIPINPUT |
21641 | 13 |
include PGIPOUTPUT |
21637 | 14 |
end |
15 |
||
16 |
structure Pgip : PGIP = |
|
17 |
struct |
|
18 |
open PgipTypes |
|
21641 | 19 |
open PgipMarkup |
21637 | 20 |
open PgipInput |
21 |
open PgipOutput |
|
22 |
end |