Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

current_axioms

Theory.current_axioms : unit -> (string * thm) list

Return the axioms in the current theory segment.

An invocation current_axioms() returns a list of the axioms asserted in the current theory segment.

Failure

Never fails. If no axioms have been asserted, the empty list is returned.

See also

Theory.current_theory, Theory.new_theory, Theory.current_definitions, Theory.current_theorems, Theory.constants, Theory.types, Theory.parents