| author | blanchet |
| Wed, 15 Sep 2010 20:07:41 +0200 | |
| changeset 39431 | f5320aba6750 |
| parent 29606 | fedb8be05f24 |
| permissions | -rw-r--r-- |
(* Title: Pure/ProofGeneral/pgip.ML Author: David Aspinall Prover-side PGIP abstraction. Not too closely tied to Isabelle, to help with reuse/porting. *) signature PGIP = sig include PGIPTYPES include PGIPMARKUP include PGIPINPUT include PGIPOUTPUT end structure Pgip : PGIP = struct open PgipTypes open PgipMarkup open PgipInput open PgipOutput end