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

judgment
  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:

  judgment
    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 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2009/doc-src/IsarRef/Thy/First_Order_Logic.thy


	Makarius





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