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.

current_theory, new_theory, current_axioms, current_theorems, constants, types, parents, new_definition, new_specification, new_type_definition, Define, Hol_reln