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 MHonArc.