holyhammer : term -> thm
STRUCTURE
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
HOL  Trindemossen-1