theorems : string -> (string * thm) list

- STRUCTURE
- SYNOPSIS
- All the theorems stored in the named theory.
- DESCRIPTION
- An invocation theorems thy, where thy is the name of a currently loaded theory segment, will return a list of the theorems stored in that theory. Axioms and definitions are excluded. 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
- theorems "combin"; > val it = [("I_o_ID", |- !f. (I o f = f) /\ (f o I = f)), ("I_THM", |- !x. I x = x), ("W_THM", |- !f x. W f x = f x x), ("C_THM", |- !f x y. combin$C f x y = f y x), ("S_THM", |- !f g x. S f g x = f x (g 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_THM", |- !f g x. (f o g) x = f (g x))] : (string * thm) list

- SEEALSO

HOL Kananaskis-13