Re: [isabelle] induction over mutually-inductively-defined predicate

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.