| author | huffman |
| Thu, 15 Jan 2009 10:00:31 -0800 | |
| changeset 29538 | 5cc98af1398d |
| parent 21641 | d73ab30e82dc |
| child 29606 | fedb8be05f24 |
| permissions | -rw-r--r-- |
| 21637 | 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 |
|
| 21641 | 12 |
include PGIPMARKUP |
| 21637 | 13 |
include PGIPINPUT |
| 21641 | 14 |
include PGIPOUTPUT |
| 21637 | 15 |
end |
16 |
||
17 |
structure Pgip : PGIP = |
|
18 |
struct |
|
19 |
open PgipTypes |
|
| 21641 | 20 |
open PgipMarkup |
| 21637 | 21 |
open PgipInput |
22 |
open PgipOutput |
|
23 |
end |