find_in

DB.find_in : string -> data list -> data list

Search for theory element by name fragment, among a given list.

An invocation DB.find_in s data_list selects from data_list those theory elements which have been stored with a name in which s occurs as a proper substring, ignoring case distinctions.

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...]

> DB.find_in "sum" it;
val it =
   [(("sum", "sum_distinct"),
     (⊢ ∀x y. INL x ≠ INR y, Thm,
      Located
       {exact = true, linenum = 259, scriptpath =
        "$(HOLDIR)/src/coretypes/sumScript.sml"})),
    (("sum", "sum_distinct1"),
     (⊢ ∀x y. INR y ≠ INL x, Thm,
      Located
       {exact = true, linenum = 269, scriptpath =
        "$(HOLDIR)/src/coretypes/sumScript.sml"}))]:
   DB_dtype.public_data_value named list

Finding theorems in interactive proof sessions. The second argument will normally be the result of a previous call to DB.find, DB.match, DB.apropos, DB.listDB, DB.thy etc.

See also

DB.find, DB.match, DB.apropos, DB.listDB, DB.thy, DB.theorems