EQF_INTRO : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Converts negation to equality with
F
.
DESCRIPTION
A |- ~tm ------------- EQF_INTRO A |- tm = F
FAILURE
Fails if the argument theorem is not a negation.
SEEALSO
EQF_ELIM
,
EQT_ELIM
,
EQT_INTRO
HOL
Kananaskis-14