[isabelle-dev] Reviving an old thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?
brianh at cs.pdx.edu
Wed Oct 12 15:24:52 CEST 2011
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.
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:
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?
More information about the isabelle-dev