`{auauto}w'

(ml, apply) Insert (<tac> THENW <tac>) with the current favorite auto tactic, which is selected intermitantly by the user with `(backspace)'. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html