find

DB.find : string -> data list

Search for theory element by name fragment.

An invocation DB.find s returns a list of theory elements which have been stored with a name containing a substring matching the regular expression s, ignoring case distinctions. All currently loaded theory segments are searched. The regular expression notation allows parentheses, dot (.) to match any character, Kleene star (*), alternation (|) and a special form of intersection (~).

The tilde form r~s is defined to be equal to (.*r.*)&(.*s.*), where & is regular expression intersection. This allows one 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,
      Located
       {exact = true, linenum = 3572, scriptpath =
        "$(HOLDIR)/src/num/theories/arithmeticScript.sml"})),
    (("arithmetic", "STRICTLY_INCREASING_ONE_ONE"),
     (⊢ ∀f. (∀n. f n < f (SUC n)) ⇒ ONE_ONE f, Thm,
      Located
       {exact = true, linenum = 4282, scriptpath =
        "$(HOLDIR)/src/num/theories/arithmeticScript.sml"})),
    (("arithmetic", "STRICTLY_INCREASING_TC"),
     (⊢ ∀f. (∀n. f n < f (SUC n)) ⇒ ∀m n. m < n ⇒ f m < f n, Thm,
      Located
       {exact = true, linenum = 4275, scriptpath =
[...Output elided...]

Finding theorems in interactive proof sessions.

See also

DB.find_in, DB.match, DB.apropos, DB.selectDB, DB.thy, DB.theorems