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