> 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}]
(Makarius suggested to continue the discussion on the Isabelle mailing list.) There is an incomplete Isabelle programming tutorial at http://isabelle.in.tum.de/nominal/activities/idp/ where the "First Steps" Section might be helpful to shed more light on antiquotations. Comments are welcome. Christian