[isabelle] Tutorial in isar-ref.pdf



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

Can anybody tell me what the correction for this tutorial is to get it to work,  or possibly where the correct tutorial resides.
I would like to use this as a demonstration of Isabelle to my compatriots.
Sincerely,

David




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