Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-01-31 12:23:20 -0800 (Wed, 31 Jan 2001)
Revision: 3123
Log message:
There was inconsistent with the documentation and the implementation
of the ifLabT and RepeatT tactics.
The documentation about ifLabT is corrected.
The old repeatT tactic is now called whileProgressT.
The (repeatT tac) is now defined as whileProgressT (tryT tac)
Still to do: implement the untilFailT tactic (Nuprl's REPEAT).
* whileProgressT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals while there is a progress.
* untilFailT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails.
* repeatT : tactic -> tactic
Repeatedly execute the given tactic on all subgoals until it fails or no more
progress is made.
See also all-theories.pdf.