----------------------------------------------------------------------
find_in                                                           (DB)
----------------------------------------------------------------------
find_in : string -> data list -> data list

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

DESCRIBE
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)),
     (("bool", "BOOL_EQ_DISTINCT"), (|- ~(T = F) /\ ~(F = T), Thm)),
     (("list", "list_distinct"), (|- !a1 a0. ~([] = a0::a1), Thm)),
     (("sum", "sum_distinct"), (|- !x y. ~(INL x = INR y), Thm)),
     (("sum", "sum_distinct1"), (|- !x y. ~(INR y = INL x), Thm))]
  : ((string * string) * (thm * class)) list

- DB.find_in "sum" it;
> val it =
    [(("sum", "sum_distinct"), (|- !x y. ~(INL x = INR y), Thm)),
     (("sum", "sum_distinct1"), (|- !x y. ~(INR y = INL x), Thm))]
  : ((string * string) * (thm * class)) list


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

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

----------------------------------------------------------------------