Lines Matching refs:clause
10 (* A type of clause sets that supports efficient subsumption checking. *)
19 val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume
32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
33 (Thm.clause * Subst.subst * 'a) option
35 val isSubsumed : 'a subsume -> Thm.clause -> bool
38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause ->
39 (Thm.clause * Subst.subst * 'a) option
41 val isStrictlySubsumed : 'a subsume -> Thm.clause -> bool
44 (* Single clause versions. *)
47 val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option
49 val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option