Passes a theorem unchanged to a theorem-tactic.
For any theorem-tactic ttac and theorem th, the application
ALL_THEN ttac th results simply in ttac th, that is, the theorem
is passed unchanged to the theorem-tactic. ALL_THEN is the identity
The application of ALL_THEN to a theorem-tactic never fails. The resulting
theorem-tactic fails under exactly the same conditions as the original one.
Writing compound tactics or tacticals, e.g. terminating list iterations