Re: [isabelle] inductive_set and ordinal induction

On 10/26/2015 06:15 PM, Andreas Lochbihler wrote:
No, I'd be glad if it was made available. Probably nobody ever invested the time to adapt the code base.


On 26/10/15 18:06, Tobias Nipkow wrote:
Bummer! Is there any reason not to make the monotonicity theorem availble in user space?
If not...


Hi all,

monotonicity and similar theorems are not made available to the user because this would expose
the inner workings of the inductive definition package, which can change without prior notice.
For a more detailed discussion of this problem, see e.g. this thread:


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