Re: [isabelle] induction over mutually-inductively-defined predicate
Yes, exactly! Christian
Lars Noschinski writes:
> On 08.11.2011 17:45, Christian Urban wrote:
> >There used to be an example theory in the Isabelle
> > distribution which explains all bells and whistles of the
> > induct-method, but I cannot find it at the moment. Maybe others
> > can point to it.
> $ISABELLE_HOME/src/HOL/Induct/Common_Patterns.thy, I guess.
> -- Lars
This archive was generated by a fusion of
Pipermail (Mailman edition) and