Re: [isabelle] Context in resolve_tac and rtac



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


> On 26 May 2015, at 11:31, Peter Lammich <lammich at in.tum.de> wrote:
> 
> 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?
> 
> --
>  Peter
> 
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.