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

Christian Urban urbanc at in.tum.de
Tue Jun 30 02:47:45 CEST 2009

> 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


where the "First Steps" Section might be helpful to shed
more light on antiquotations. Comments are welcome.


More information about the isabelle-dev mailing list