don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
(* 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