holyhammer : term -> thm
STRUCTURE
holyHammer
SYNOPSIS
A call to the rule
holyHammer.holyhammer
on a term
tm
is equivalent to a call to the tactic
holyHammer.hh
on the goal
([],tm)
.
SEEALSO
hh
HOL
Kananaskis-13