Re: [isabelle] Tutorial in isar-ref.pdf

On Fri, 4 Sep 2009, Dave Thayer wrote:

In the Isabelle/Isar Reference Manual from the documents section on the Isabelle page there is an example of First Order Logic (Section 2.3) however when I get to the expression

  Trueprop :: "o => prop"  (_ 5);

I am getting the error

*** Outer syntax error:  keyword "infix" expected,
*** but symbolic identifier _ was found

The true source reads like this:

    Trueprop :: "o \<Rightarrow> prop"    ("_" 5)

The manuals usually prefer nice "pretty printing" over direct copy-paste support. This is an old issue of LaTeX typesetting -- even with the crude typewriter style pasting usually breaks down.

Luckily, more recent additions to PDF (and pdflatex) seem to allow certain internal coding annotations that would paste the above ASCII version if copied from the nicely typeset text. We are still working on making this available routinely.

In the meantime you can get the document raw sources from


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