`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