Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-09 17:52:47 -0700 (Wed, 09 Jun 2004)
Revision: 5871
Log message:
Added a "find_subgoal" tool for finding the primitive node that generated
the given subgoal. This should be a great tactic debugging tool.
Basically, when you at a node (whether a rule box, or an internal "address 0"
one) on the form
Goal Term
BY ...
1. Subgoal Term
2. Subgoal Term
...
then "find_subgoal 0" would take you to the node that generated the goal term
(i.e. it would go up towards the root of the proof tree), the "find_subgoal 1"
would take you to the node that _first_ generated the subgoal 1 term (if
goal happens to be the same as subgoal 1, then it would still go up the tree;
otherwise it would "zoom into" the current node).
P.S. This code is not fully debugged, there still might be an "off by one" error
somewhere.