src/Pure/ProofGeneral/pgip.ML
author wenzelm
Tue, 14 Feb 2012 20:57:05 +0100
changeset 46470 b0331b0d33a3
parent 29606 fedb8be05f24
permissions -rw-r--r--
discontinued unused MRL -- in correspondence with section "2.4.2 Rule composition" in the implementation manual;

(*  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