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
