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 polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml