On Wed, 12 Oct 2011, Brian Huffman wrote:
After implementing the warning, I dug through the revision history and
was surprised to find that my "new" feature actually used to exist! It
was removed in January 2006:
http://isabelle.in.tum.de/repos/isabelle/rev/ca56111fe69c
I don't understand why the warning message was ever removed. The
commit message "fix_tac: no warning" is unhelpful.
This needs some further investigation. My log message from 2006 is an
example of how not to do it -- just parroting the change without any
explanation. (2006 was a bad year in Isabelle development.)
Does your own change do anything different from the old version?
BTW, that one was originating from here:
http://isabelle.in.tum.de/repos/isabelle/rev/dfe5d09514eb
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
