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

USES
Finding theorems in interactive proof sessions.
SEEALSO
find_in, match, apropos, thy, theorems
HOL  Kananaskis-14