equal
deleted
inserted
replaced
10 |
10 |
11 consts |
11 consts |
12 Diophant'_equation :: "[bool, int, bool ] |
12 Diophant'_equation :: "[bool, int, bool ] |
13 => bool " |
13 => bool " |
14 ("((Script Diophant'_equation (_ _ =))//(_))" 9) |
14 ("((Script Diophant'_equation (_ _ =))//(_))" 9) |
15 axioms(*axiomatization where*) |
|
16 |
15 |
|
16 axiomatization where |
17 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" |
17 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" |
18 |
18 |
19 ML {*val thy = @{theory}*} |
19 ML {*val thy = @{theory}*} |
20 |
20 |
21 text {*problemclass for the usecase*} |
21 text {*problemclass for the usecase*} |