return to top
source
This RuleTac is applied once to the root goal, before any other rules are tried.
RuleTac