Lines Matching refs:pair
163 (* pairlike p x: takes a pair structure p and a term x. *)
236 (* instances of the bound pair p and it subcomponents. *)
450 (* If the argument of the resulting conversion is a pair, this conversion *)
451 (* recursively applies itself to both sides of the pair. *)
782 failwith "bound pair occurs in both conjuncts"
931 failwith "bound pair occurs in both conjuncts"
1098 failwith "bound pair occurs in both sides of `==>`"
1237 failwith "bound pair occurs in both sides of `==>`"
1987 raise ERR"P_SKOLEM_CONV" "first argument not a variable pair"
2016 "existential variable not of pair type"
2414 raise ERR "PMATCH_MP_TAC" "generalized pair(s)"