theory Superposition_Example imports Superposition IsaFoR_Term_Copy begin (* TODO: Add more examples *) abbreviation trivial_select :: "'a clause ⇒ 'a clause" where "trivial_select _ ≡ {#}" abbreviation trivial_tiebreakers where "trivial_tiebreakers _ _ _ ≡ False" abbreviation unit_types where "unit_types _ ≡ ([], ())"