Email Gateway (Aug 18 2022 at 14:01): Email Gateway (Aug 18 2022 at 14:01):From: Dave Thayer <dathayer@microsoft.com>
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
Email Gateway (Aug 18 2022 at 14:01):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 14:02):From: Makarius <makarius@sketis.net>
Yes, this is the plain ASCII replacement for this symbol.
Makarius
Email Gateway (Aug 18 2022 at 14:02):From: Dave Thayer <dathayer@microsoft.com>
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?
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
Last updated: Apr 18 2024 at 20:16 UTC