[isabelle-dev] Spec_Check

Lukas Bulwahn bulwahn at in.tum.de
Thu May 30 17:35:03 CEST 2013

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.


More information about the isabelle-dev mailing list