theory Ground_Clause imports Saturation_Framework_Extensions.Clausal_Calculus Ground_Term_Extra Ground_Context Uprod_Extra begin type_synonym 'f gatom = "'f gterm uprod" end