DEFAULT-OB is a flag or parameter.
If DEEPEST, the default next obligation is found by depth-first
search of the obtree, if HIGHEST it is found by breadth-first-search,
if D-SMALLEST then the deepest of the set of smallest obligations (i.e.
the set of all obligations with the fewest possible literals) is
chosen, if H-SMALLEST then the highest of this set is chosen.
DEFAULT-OB takes values of type OBDEFAULT.
It belongs to subjects ETREES MTREE-TOP .
Its default value is D-SMALLEST
Its current value is D-SMALLEST.

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage