current_theorems : unit -> (string * thm) list
STRUCTURE
SYNOPSIS
Return the theorems stored in the current theory segment.
DESCRIPTION
An invocation current_theorems () returns the list of theorems stored in the current theory segment.
FAILURE
Never fails. If no theorems have been stored, the empty list is returned.
SEEALSO
HOL  Kananaskis-13