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 Kananaskis-13