[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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and