Change full format of TS-expressions from "@[ev](f,o,U)" to "@[ev][f,o,U]",
because we are using the brackets to indicate LF-application.

Add tactics "fail" and "admit" (experimental).