find : string -> data list
STRUCTURE
DB
SYNOPSIS
Search for theory element by name fragment.
DESCRIPTION
An invocation DB.find s returns a list of theory elements which have been stored with a name in which s occurs as a proper substring, ignoring case distinctions. All currently loaded theory segments are searched. The string s may use the tilde ~ operator to require multiple sub-string matches: in a string such as s1~s2, matches will be found if the name contains both s1 and s2, in either order.
FAILURE
Never fails. If nothing suitable can be found, the empty list is returned.
EXAMPLE
- DB.find "inc";
val it =
    [(("arithmetic", "MULT_INCREASES"),
      (⊢ ∀m n. 1 < m ∧ 0 < n ⇒ SUC n ≤ m * n, Thm)),
     ...
     (("list", "ALL_DISTINCT_EL_IMP"),
      (⊢ ∀l n1 n2.
          ALL_DISTINCT l ∧ n1 < LENGTH l ∧ n2 < LENGTH l ⇒
          (EL n1 l = EL n2 l ⇔ n1 = n2), Thm)),
     ...] : public_data list
> DB.find "ass~conj";
val it =
   [(("bool", "CONJ_ASSOC"),
     (⊢ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3, Thm)),
    (("combin", "ASSOC_CONJ"), (⊢ ASSOC $/\, Thm))]: public_data list

USES
Finding theorems in interactive proof sessions.
SEEALSO
find_in, match, apropos, selectDB, thy, theorems
HOL  Trindemossen-1