On Jun 29, 2009, at 10:10 PM, Dave Thayer wrote:
Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing
about them. Isabelle preprocesses the ML files it read and replaces
the antiquotations before passing on the code to the PolyML compiler.
Steven
I am working with the Isabell/HOL system which is hosted by default
on the PolyML system. I have found a strange syntax construct in
some of the source code files consisting of @{ ...some
verbage ... } , examples below. I have searched the ML library
pages and the PolyML docs looking for this syntactical construct and
have been unable to find it. Does anyone know what this signifies?
let metaSubst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x
\<equiv> t \<Longrightarrow> PROP P x)" by (unfold propDef)}
[...@{thm propDef}]
Thanks
David Thayer
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
