definitions

DB.definitions : string -> (string * thm) list

All the definitions stored in the named theory.

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 =
   [("W_DEF", ⊢ W = (λf x. f x x)),
    ("UPDATE_def", ⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)),
    ("S_DEF", ⊢ S = (λf g x. f x (g x))),
    ("RIGHT_ID_DEF", ⊢ ∀f e. RIGHT_ID f e ⇔ ∀x. f x e = x),
    ("RESTRICTION", ⊢ ∀s f x. RESTRICTION s f x = if x ∈ s then f x else ARB),
    ("o_DEF", ⊢ ∀f g. f ∘ g = (λx. f (g x))),
    ("MONOID_DEF", ⊢ ∀f e. MONOID f e ⇔ ASSOC f ∧ RIGHT_ID f e ∧ LEFT_ID f e),
    ("LEFT_ID_DEF", ⊢ ∀f e. LEFT_ID f e ⇔ ∀x. f e x = x),
    ("K_DEF", ⊢ K = (λx y. x)), ("I_DEF", ⊢ I = S K K),
    ("FCOMM_DEF", ⊢ ∀f g. FCOMM f g ⇔ ∀x y z. g x (f y z) = f (g x y) z),
    ("FAIL_DEF", ⊢ FAIL = (λx y. x)),
    ("EXTENSIONAL_def", ⊢ ∀s f. EXTENSIONAL s f ⇔ ∀x. x ∉ s ⇒ f x = ARB),
    ("COMM_DEF", ⊢ ∀f. COMM f ⇔ ∀x y. f x y = f y x),
    ("C_DEF", ⊢ flip = (λf x y. f y x)),
[...Output elided...]

See also

DB.thy, DB.fetch, DB.thms, DB.theorems, DB.axioms, DB.listDB