matcher : (term -> term -> 'a) -> string list -> term -> data list
STRUCTURE
SYNOPSIS
All theory elements matching a given term.
DESCRIPTION
An invocation matcher pm [thy1,...,thyn] M collects all elements of the theory segments thy1,...,thyn that have a subterm N such that pm M does not fail (raise an exception) when applied to N. Thus matcher potentially traverses all subterms of all theorems in all the listed theories in its search for ‘matches’.

If the list of theory segments is empty, then all currently loaded segments are examined. The string "-" may be used to designate the current theory segment.

FAILURE
Never fails, but may return an empty list.
EXAMPLE
- DB.matcher match_term ["relation"] (Term `P \/ Q`);
> val it =
    [(("relation", "RC_def"), (|- !R x y. RC R x y = (x = y) \/ R x y, Def)),
     (("relation", "RTC_CASES1"),
      (|- !R x y. RTC R x y = (x = y) \/ ?u. R x u /\ RTC R u y, Thm)),
     (("relation", "RTC_CASES2"),
      (|- !R x y. RTC R x y = (x = y) \/ ?u. RTC R x u /\ R u y, Thm)),
     (("relation", "RTC_TC_RC"),
      (|- !R x y. RTC R x y ==> RC R x y \/ TC R x y, Thm)),
     (("relation", "TC_CASES1"),
      (|- !R x z. TC R x z ==> R x z \/ ?y. R x y /\ TC R y z, Thm)),
     (("relation", "TC_CASES2"),
      (|- !R x z. TC R x z ==> R x z \/ ?y. TC R x y /\ R y z, Thm))] :
  ((string * string) * (thm * class)) list

- DB.matcher (ho_match_term [] empty_varset) [] (Term `?x. P x \/ Q x`);
<<HOL message: inventing new type variable names: 'a>>
> val it =
    [(("arithmetic", "ODD_OR_EVEN"),
      (|- !n. ?m. (n = SUC (SUC 0) * m) \/ (n = SUC (SUC 0) * m + 1), Thm)),
     (("bool", "EXISTS_OR_THM"),
      (|- !P Q. (?x. P x \/ Q x) = (?x. P x) \/ ?x. Q x, Thm)),
     (("bool", "LEFT_OR_EXISTS_THM"),
      (|- !P Q. (?x. P x) \/ Q = ?x. P x \/ Q, Thm)),
     (("bool", "RIGHT_OR_EXISTS_THM"),
      (|- !P Q. P \/ (?x. Q x) = ?x. P \/ Q x, Thm)),
     (("sum", "IS_SUM_REP"),
      (|- !f.
            IS_SUM_REP f =
            ?v1 v2.
              (f = (\b x y. (x = v1) /\ b)) \/ (f = (\b x y. (y = v2) /\ ~b)),
       Def))] : ((string * string) * (thm * class)) list

COMMENTS
Usually, pm will be a pattern-matcher, but it need not be.
SEEALSO
HOL  Kananaskis-14