Re: [isabelle] basic example causes error message

Are you sure you use the right tick character? 
It should be 'a, not ’a.


p.s. This always happens to me when copy-pasting material from pdf, as
most pdf-viewers seem to use OCR to reconstruct the text from the

On Di, 2012-07-03 at 20:27 +0200, Gergely Buday wrote:
> Hi,
> I have installed the official Isabelle release, and tried the
> following example from Programming and Proving:
> theory MyList
> imports Main
> begin
> datatype ’a list = Nil | Cons ’a "’a list"
> fun app :: "’a list => ’a list => ’a list" where
> "app Nil ys = ys" |
> "app (Cons x xs) ys = Cons x (app xs ys)"
> fun rev :: "’a list => ’a list" where
> "rev Nil = Nil" |
> "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
> value "rev(Cons True (Cons False Nil))"
> end
> now, at the datatype declaration jedit shows an error sign and the output says
> Outer syntax error: name declaration expected,
> but bad input ’a was found
> What is the problem here?
> - Gergely

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