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

[Makarius]

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).


 	Makarius