[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

Makarius makarius at sketis.net
Wed Feb 9 10:57:45 CET 2011

On Wed, 9 Feb 2011, Gerwin Klein wrote:

> I don't mind either way, but I'd like to point out that the _tac 
> instantiations are everything but out of fashion. I'm fully aware that 
> they are bad style, rely on dynamic names, etc, but there is no way 
> around them if you write apply style.

Having observed the conceptual problems already many years ago, I am also 
fully aware that the res_inst_tac variants still occur in practically 
important proof script.  At some point one should seriously revisit the 
question why this is so, and what needs to be done to make a significant 
step forward (away from adhoc instantiations).


More information about the isabelle-dev mailing list