holyhammer

holyHammer.holyhammer : term -> thm

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).

See also

holyHammer.hh