On Wed, Oct 12, 2011 at 4:01 PM, Makarius <[email protected]> wrote: > 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.)
I can think of two potential reasons for dropping the warning: First, since fix_tac is an exported function, it might be used by other tactics besides induction. If the warning is triggered in other contexts, the wording of the message might be inappropriate or misleading. Second, it is possible that induction with "arbitrary" variables might be used by other ML packages for internal proofs. Warnings are obviously not helpful for users if they were not caused by those users' proof scripts. > Does your own change do anything different from the old version? The warning message is worded differently, but otherwise my changeset is almost exactly the reverse of ca56111fe69c. - Brian _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
