[isabelle] Defining Recursive Functions in Isabelle/HOL

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 

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.