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