Theory.current

current_axioms : unit -> (string * thm) list

STRUCTURE: Theory
SYNOPSIS: Return the axioms in the current theory segment.
DESCRIPTION: 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.
SEEALSO: current_theory, new_theory, current_definitions, current_theorems, constants, types, parents

HOL Trindemossen-1