definitions : string -> (string * thm) list
STRUCTURE
DB
SYNOPSIS
All the definitions stored in the named theory.
DESCRIPTION
An invocation definitions thy, where thy is the name of a currently loaded theory segment, will return a list of the definitions stored in that theory. Each definition is paired with its name in the result. The string "-" may be used to denote the current theory segment.
FAILURE
Never fails. If thy is not the name of a currently loaded theory segment, the empty list is returned.
EXAMPLE
- definitions "combin";
> val it =
    [("C_DEF", |- combin$C = (\f x y. f y x)),
     ("I_DEF", |- I = S K K),
     ("K_DEF", |- K = (\x y. x)),
     ("o_DEF", |- !f g. f o g = (\x. f (g x))),
     ("S_DEF", |- S = (\f g x. f x (g x))),
     ("W_DEF", |- W = (\f x. f x x))] : (string * thm) list

SEEALSO
thy, fetch, thms, theorems, axioms, listDB
HOL  Kananaskis-13