[isabelle-dev] Spec_Check

[Makarius]

On Thu, 30 May 2013, Lukas Bulwahn wrote:

> I was thinking of a ML antiquotation for "check_property @{context}"  and I 
> was thinking of @{spec ...} and some context flags that lets spec either only 
> compile, or check with values.
> This should allow that @{spec ...} could be inlined in the implementation if 
> anyone wishes to do so.

Do you know how to define the ML antiquotation, or shall I do it?


 	Makarius