Theory Selection_Function

theory Selection_Function
  imports
    Ground_Clause
begin

locale select =
  fixes sel :: "'a clause ⇒ 'a clause"
  assumes
    select_subset: "⋀C. sel C ⊆# C" and
    select_negative_lits: "⋀C L. L ∈# sel C ⟹ is_neg L"

end