[isabelle-dev] Spec_Check

[Lukas Bulwahn]

On 05/30/2013 05:32 PM, Makarius wrote:
> 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?
>
Please go ahead and do it when you have time.

Lukas