fetch : string -> string -> thm

- STRUCTURE
- SYNOPSIS
- Fetch a theorem by theory and name.
- DESCRIPTION
- 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

- SEEALSO

HOL Kananaskis-13