29 Jun
2009
29 Jun
'09
10:10 p.m.
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