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



Thank you that is working.  I had figured out that I had to add the quotes on the expression but I had not realized I had to add the quotes on the mixfix operator.  I have found that on my system I don't have to use "\<Rightarrow>" but can use "=>" is that kosher?

-----Original Message-----
From: Makarius [mailto:makarius at sketis.net] 
Sent: Saturday, September 05, 2009 12:46 PM
To: Dave Thayer
Cc: cl-isabelle-users at lists.cam.ac.uk
Subject: 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.