[isabelle-dev] [polyml] Strange syntax in PolyML Code

[Christian Urban]

> 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