Theory.current

current_thms : unit -> (string * thm) list

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

HOL Kananaskis-10