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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
