Re: [polyml] Strange syntax in PolyML Code

2009-06-29 Thread Makarius
On Mon, 29 Jun 2009, Steven Obua wrote: Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing about them. Isabelle preprocesses the ML files it read and replaces the antiquotations before passing on the code to the PolyML compiler. BTW, since people have asked this before: in I

Re: [polyml] Strange syntax in PolyML Code

2009-06-29 Thread Steven Obua
On Jun 29, 2009, at 10:10 PM, Dave Thayer wrote: Hi, the "@" syntax is called an Anti-Quotation. PolyML knows nothing about them. Isabelle preprocesses the ML files it read and replaces the antiquotations before passing on the code to the PolyML compiler. Steven I am working with the Isa

[polyml] Strange syntax in PolyML Code

2009-06-29 Thread Dave Thayer
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 th