*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] inductive_set and ordinal induction*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 27 Oct 2015 09:56:45 +0100*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>, Tobias Nipkow <nipkow at in.tum.de>*In-reply-to*: <562F37C2.5000308@in.tum.de>*References*: <561F736D.9070902@yozora.eu> <562E25F4.2070509@yozora.eu> <562E580C.3020305@in.tum.de> <562E5B48.5070703@inf.ethz.ch> <562E5D96.9010402@in.tum.de> <562E5FCD.4040802@inf.ethz.ch> <562F37C2.5000308@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Stefan,

Something similar can also be useful for the inductive package, as this request shows.

Best, Andreas On 27/10/15 09:37, Stefan Berghofer wrote:

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

**Follow-Ups**:**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**References**:**[isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Christoph Dittmann

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Tobias Nipkow

**Re: [isabelle] inductive_set and ordinal induction***From:*Andreas Lochbihler

**Re: [isabelle] inductive_set and ordinal induction***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] inductive_set and ordinal induction
- Next by Date: Re: [isabelle] inductive_set and ordinal induction
- Previous by Thread: Re: [isabelle] inductive_set and ordinal induction
- Next by Thread: Re: [isabelle] inductive_set and ordinal induction
- Cl-isabelle-users October 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list