The function flatn is part of the subgoal package. For a general description of the subgoal package, see set_goal.

The flatn function’s basic step of operation is to take the the current list of sub-goals and concatenate it with the previous list of subgoals (excluding the first of that list, from which the current list was obtained). The numeric argument passed to flatn specifies how many times this operation is to be performed.

Raises the NO_PROOFS exception if there is no current proof manipulated by the subgoal package.

If n is too large, or negative, the result will be a flat list of all subgoals.

set_goal, restart, backup, restore, save, set_backup, expand, expandf, p, top_thm, top_goal