Hello all, This is a follow-up to the conversation on the isabelle-users list from a few months ago, about confusion that arises when using mutual induction with the "arbitrary" option.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-June/msg00001.html At the time I suggested that their ought to be a warning message when you specify an "arbitrary" variable, if that variable does not actually appear in the goal. Today I finally tried implementing this warning message; it turns out that it requires only a simple modification to function fix_tac in src/Tools/induct.ML. 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. Is there any good reason why we shouldn't put the warning back in? - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
