[isabelle-dev] Reviving an old thread: [isabelle] structured induction: mutual definitions and "arbitrary" in inductions?

[Makarius]

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