*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] The "inductive" command loops*From*: Joachim Breitner <breitner at kit.edu>*Date*: Mon, 09 Feb 2015 16:10:03 +0100

Hi, the declaration inductive foo :: "int â bool" where "P x â foo x" -- "note the free P!" makes the system loop during "Proving the simplification rules ...". Such an inductive predicate is probably not very useful, but it maybe it is still possible to make "inductive" a mit more robust in this respect? Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] The "inductive" command loops***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
- Next by Date: [isabelle] Code generator produces non-linear patterns
- Previous by Thread: Re: [isabelle] Discharging non-atomic assumptions in Isabelle/ML
- Next by Thread: Re: [isabelle] The "inductive" command loops
- Cl-isabelle-users February 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