Hi Johannes,
I have often run into this problem myself, too, especially in case of non-termination. I
would find it sensible that code_abort deletes the code equation.
Andreas
On 09/07/13 15:28, Johannes Hölzl wrote:
Hi *,
code_abort does not remove the corresponding code equations
(in Isab
Hi *,
code_abort does not remove the corresponding code equations
(in Isabelle 19764bef2730)
definition "test = True"
code_abort test
value [code] test -- "outputs True"
definition [code del]: "test2 = True"
code_abort test2
value [code] test2 -- "raises 'test' exception"
Should cod
On Mon, 2013-07-08 at 11:09 +0200, Makarius wrote:
> Does the Isabelle tool "dimacs2hol" from 2004 still have a purpose?
>
> The DIMACS CNF format appears to be an old proposal for SAT, predating
> newer things like SMT-LIB. So this looks like a candidate for deletion.
DIMACS CNF remains the st
