[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
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