EQT_INTRO : thm -> thm
STRUCTURE
Drule
SYNOPSIS
Introduces equality with
T
.
DESCRIPTION
A |- tm ------------- EQT_INTRO A |- tm = T
FAILURE
Never fails.
SEEALSO
EQT_ELIM
,
EQF_ELIM
,
EQF_INTRO
HOL
Kananaskis-11