*To*: "gallais @ ensl.org" <guillaume.allais at ens-lyon.org>*Subject*: Re: [isabelle] Non terminating function proven terminating*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sun, 23 Oct 2011 00:53:32 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CADW2s6KOER_Nmwj0oCtNcMwzRNK7i=g5AA3VQmjznBi81qykxQ@mail.gmail.com>*References*: <CADW2s6KOER_Nmwj0oCtNcMwzRNK7i=g5AA3VQmjznBi81qykxQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20111004 Icedove/3.0.11

I did not find Isabelle's bug tracker so I hope that this is the place where I'm supposed to report this.

Pierre Boutillier's trick (which breaks Coq's SN) seems to work in Isabelle. As in Agda, we do not lose SN but we do accept a function that is not well-defined.

Some further remarks:

Alex

**References**:**[isabelle] Non terminating function proven terminating***From:*gallais @ ensl.org

- Previous by Date: Re: [isabelle] Declaring global attributes
- Next by Date: [isabelle] FICS 2012 Call for Papers
- Previous by Thread: Re: [isabelle] Non terminating function proven terminating
- Next by Thread: Re: [isabelle] Better way to beta apply two terms
- Cl-isabelle-users October 2011 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