Re: [isabelle] inductive_set and ordinal induction



On 10/27/2015 09:56 AM, Andreas Lochbihler wrote:
> You are right in that the rules generated by the inductive package
> suffice for proving.

I don't see how ordinal induction (like lfp_ordinal_induct)
  "[| ... |] ==> P X"
is derivable from the pointwise induction rule
  "[| X x; ... |] ==> P x"
provided by the inductive package.

Or is it derivable?

Best,
Christoph





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.