| author | wenzelm | 
| Wed, 15 Jun 2011 16:22:58 +0200 | |
| changeset 43397 | dba359c0ae3b | 
| 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 |