*To*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Subject*: Re: [isabelle] Defining Recursive Functions in Isabelle/HOL*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 27 Nov 2008 11:32:09 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <608872.91692.qm@web84006.mail.mud.yahoo.com>*References*: <608872.91692.qm@web84006.mail.mud.yahoo.com>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias TIMOTHY KREMANN wrote:

I have entered everything from page 13 exactly as in the paper (except added "" where necessary). And I get the following message from line 18 (counting the blank line): *** Unknown fact "\<langle>f n \<noteq> 0\<rangle>" *** At command "with". I have switched the angle brackets to parens and to blanks and still get a similar message. What have I missed? (You get to this paper from the Isabelle Documentation page via the "Tutorial of Function Definitions" link)Thanks, Tim

**References**:**[isabelle] Defining Recursive Functions in Isabelle/HOL***From:*TIMOTHY KREMANN

- Previous by Date: [isabelle] Defining Recursive Functions in Isabelle/HOL
- Next by Date: Re: [isabelle] about longer computation syntax sugar
- Previous by Thread: [isabelle] Defining Recursive Functions in Isabelle/HOL
- Next by Thread: [isabelle] load HOL4
- Cl-isabelle-users November 2008 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