axioms : string -> (string * thm) list

- STRUCTURE
- SYNOPSIS
- All the axioms stored in the named theory.
- DESCRIPTION
- An invocation axioms thy, where thy is the name of a currently loaded theory segment, will return a list of the 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
- axioms "bool"; > val it = [("INFINITY_AX", |- ?f. ONE_ONE f /\ ~ONTO f), ("SELECT_AX", |- !P x. P x ==> P ($@ P)), ("ETA_AX", |- !t. (\x. t x) = t), ("BOOL_CASES_AX", |- !t. (t = T) \/ (t = F))] : (string * thm) list

- SEEALSO

HOL Kananaskis-13