fetch
DB.fetch : string -> string -> thm
Fetch a theorem by theory and name.
An invocation fetch thy name searches through the currently loaded
theory segments in an attempt to find a theorem, axiom, or definition
stored under name in theory thy.
Failure
If the specified theorem, axiom, or definition cannot be located.
Example
> DB.fetch "bool" "NOT_FORALL_THM";
val it = ⊢ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x: thm