Contains various macros for pattern matching on HOL terms.
Summary
Functions
Matches a term representing the conjunction of p_id and q_id.
Matches a term representing the disjunction of p_id and q_id.
Matches a term representing the equality of p_id and q_id.
Matches a term representing the equivalence of p_id and q_id.
Matches a term representing the universal quantification of the predicate
body_id.
Matches a term representing falsity.
Matches a term representing the implication of p_id and q_id, i.e. p
implies q.
Matches a term representing the negation of term_id.
Matches a term representing truth.
Matches a term representing the equality of p_id and q_id with respect to
their type.
Matches a term representing the universal quantification of the predicate
body_id with respect to the element type type.
Matches a term representing the universal quantification of the predicate
body_id with respect to the element type type.
Matches a term representing the universal quantification of the predicate
body_id.
Functions
Matches a term representing the conjunction of p_id and q_id.
Matches a term representing the disjunction of p_id and q_id.
Matches a term representing the equality of p_id and q_id.
Matches a term representing the equivalence of p_id and q_id.
Matches a term representing the universal quantification of the predicate
body_id.
Matches a term representing falsity.
Matches a term representing the implication of p_id and q_id, i.e. p
implies q.
Matches a term representing the negation of term_id.
Matches a term representing truth.
Matches a term representing the equality of p_id and q_id with respect to
their type.
Matches a term representing the universal quantification of the predicate
body_id with respect to the element type type.
Matches a term representing the universal quantification of the predicate
body_id with respect to the element type type.
Matches a term representing the universal quantification of the predicate
body_id.