axioms

DB.axioms : string -> (string * thm) list

All the axioms stored in the named theory.

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 =
   [("SELECT_AX", ⊢ ∀P x. P x ⇒ P ($@ P)),
    ("INFINITY_AX", ⊢ ∃f. ONE_ONE f ∧ ¬ONTO f),
    ("ETA_AX", ⊢ ∀t. (λx. t x) = t),
    ("BOOL_CASES_AX", ⊢ ∀t. (t ⇔ T) ∨ (t ⇔ F))]: (string * thm) list

See also

DB.thy, DB.fetch, DB.thms, DB.theorems, DB.definitions, DB.listDB