Email Gateway (Aug 22 2022 at 09:55): Email Gateway (Aug 22 2022 at 09:55):From: Peter Lammich <lammich@in.tum.de>
Hi,
what is the difference between "rtac thm" and "resolve_tac ctxt [thm]" ?
Why does the former tactic take no context, while the latter does, and
when should I use which tactic?
Email Gateway (Aug 22 2022 at 09:55):From: Larry Paulson <lp15@cam.ac.uk>
I am surprised that rtac and its friends still exist. They date from an era before we had any sort of IDE, and even before any of us realise that common commands can be abbreviated within Emacs. The one and only purpose of rtac, dtac, etc., was for typing fewer characters. Given the pervasive role of contexts now, I would guess that these relics should never be used in new code, and should be gradually removed from existing code.
Larry Paulson
Last updated: Apr 19 2024 at 08:19 UTC