current_definitions : unit -> (string * thm) list
STRUCTURE
SYNOPSIS
Return the definitions in the current theory segment.
DESCRIPTION
An invocation current_definitions() returns the list of definitions stored in the current theory segment. Every definition is automatically stored in the current segment by the primitive definition principles.

Advanced definition principles are built in terms of the primitives, so they also store their results in the cuurent segment. However, the definitions may be quite far removed from the user input, and they may also store some consequences of the definition as theorems.

FAILURE
Never fails. If no definitions have been made, the empty list is returned.
SEEALSO
HOL  Kananaskis-14