Theory Ground_Clause

theory Ground_Clause
  imports
    Saturation_Framework_Extensions.Clausal_Calculus

    Ground_Term_Extra
    Ground_Ctxt_Extra
    Uprod_Extra
begin

abbreviation Pos_Upair (infix "≈" 66) where
  "Pos_Upair x y ≡ Pos (Upair x y)"

abbreviation Neg_Upair (infix "!≈" 66) where
  "Neg_Upair x y ≡ Neg (Upair x y)"

type_synonym 'f gatom = "'f gterm uprod"

no_notation subst_compose (infixl "∘⇩s" 75)
no_notation subst_apply_term (infixl "⋅" 67)



end