Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Defining Recursive Functions in Isabelle/HOL

Email Gateway (Aug 18 2022 at 12:40):

From: TIMOTHY KREMANN <twksoa262@verizon.net>
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

Email Gateway (Aug 18 2022 at 12:40):

From: Tobias Nipkow <nipkow@in.tum.de>
I'm afraid that what looks similar to \<langle> ... \<rangle> are French
quotes which is what Isabelle's latex converter turns two backquotes
into: .... So that's what you need to type. A bit confusing, I agree.

Tobias

TIMOTHY KREMANN wrote:

Last updated: May 03 2024 at 08:18 UTC