*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Running a function defined in Isabelle*From*: David Cock <david.cock at inf.ethz.ch>*Date*: Fri, 23 Jan 2015 10:20:36 +0100*In-reply-to*: <CANVf7NVQ84VQSwmvz7UwT27G2aOmDY5QD5cRxdotfCP1JhUpNA@mail.gmail.com>*References*: <CANVf7NVQ84VQSwmvz7UwT27G2aOmDY5QD5cRxdotfCP1JhUpNA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.3.0

On 22/01/15 23:53, Bob Fang wrote:

Hi all, Just wondering if I have defined a function in Isabelle, is there anyway to write some simple test cases on my own first instead of jumping directly into proving properties of it?

Also, if I have proved a theorem, is it automatically added to the rewriting rules or I have to add "[simp]:" in the theorem declaration?

David Cock

**Follow-Ups**:**Re: [isabelle] Running a function defined in Isabelle***From:*Christian Sternagel

**References**:**[isabelle] Running a function defined in Isabelle***From:*Bob Fang

- Previous by Date: [isabelle] Running a function defined in Isabelle
- Next by Date: Re: [isabelle] Running a function defined in Isabelle
- Previous by Thread: [isabelle] Running a function defined in Isabelle
- Next by Thread: Re: [isabelle] Running a function defined in Isabelle
- Cl-isabelle-users January 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