Theory.current

current_defs : unit -> (string * thm) list

STRUCTURE: Theory
SYNOPSIS: Return the definitions in the current theory segment.
DESCRIPTION: An invocation current_defs () returns a list of the definitions made in the current theory segment.
FAILURE: Never fails. If no definitions have been made, the empty list is returned.
SEEALSO: current_theory, new_theory, current_axioms, current_thms, constants, types, parents

HOL Kananaskis-10