(* DL.thy
Display logic - generic features
*)
DL = Pure +
classes
term < logic
default
term
types
structure
formula
struct
arities
structure :: term
formula :: term
consts
(* Structural Connectives *)
"Sequent" :: "[structure, structure] => prop"
(* Coercing formula to structure *)
Structform :: "formula => structure"
end