changeset 52148 | aabc6c8e930a |
parent 42425 | da7fbace995b |
child 55339 | cccd24e959ba |
1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Fri Oct 18 14:36:51 2013 +0200 1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Mon Oct 21 09:03:50 2013 +0200 1.3 @@ -12,8 +12,8 @@ 1.4 Diophant'_equation :: "[bool, int, bool ] 1.5 => bool " 1.6 ("((Script Diophant'_equation (_ _ =))//(_))" 9) 1.7 -axioms(*axiomatization where*) 1.8 1.9 +axiomatization where 1.10 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" 1.11 1.12 ML {*val thy = @{theory}*}