----------------------------------------------------------------------
flatn                                                (proofManagerLib)
----------------------------------------------------------------------
flatn : int -> unit

SYNOPSIS
Flattens the tree structure of subgoals on the subgoal package goal stack.

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

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

USES
To view, reorder, or attack simultaneously,
current and previously obtained subgoals.

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

----------------------------------------------------------------------