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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
