thms : string -> (string * thm) list
STRUCTURE
SYNOPSIS
All the theorems, definitions, and axioms stored in the named theory.
DESCRIPTION
An invocation thms thy, where thy is the name of a currently loaded theory segment, will return a list of the theorems, definitions, and axioms stored in that theory. Each theorem 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
- thms "combin";
> val it =
    [("C_DEF", |- combin$C = (\f x y. f y x)),
     ("C_THM", |- !f x y. combin$C f x y = f y x), ("I_DEF", |- I = S K K),
     ("I_o_ID", |- !f. (I o f = f) /\ (f o I = f)), ("I_THM", |- !x. I x = x),
     ("K_DEF", |- K = (\x y. x)), ("K_THM", |- !x y. K x y = x),
     ("o_ASSOC", |- !f g h. f o g o h = (f o g) o h),
     ("o_DEF", |- !f g. f o g = (\x. f (g x))),
     ("o_THM", |- !f g x. (f o g) x = f (g x)),
     ("S_DEF", |- S = (\f g x. f x (g x))),
     ("S_THM", |- !f g x. S f g x = f x (g x)),
     ("W_DEF", |- W = (\f x. f x x)), ("W_THM", |- !f x. W f x = f x x)] :
  (string * thm) list

SEEALSO
HOL  Trindemossen-1