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.

Andreas

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

Tobias

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:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-May/msg00079.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-June/msg00013.html

Greetings,
Stefan




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