DB.find

STRUCTURE

SYNOPSIS

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

DESCRIPTION

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

find, match, apropos, listDB, thy, theorems