branch | decompose-isar |
changeset 42197 | 7497ff20f1e8 |
parent 41931 | ca6aac81b893 |
child 42211 | 51c3c007d7fd |
1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Mon Jul 25 08:32:32 2011 +0200 1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 13:27:59 2011 +0200 1.3 @@ -12,7 +12,7 @@ 1.4 Diophant'_equation :: "[bool, int, bool ] 1.5 => bool " 1.6 ("((Script Diophant'_equation (_ _ =))//(_))" 9) 1.7 -axioms 1.8 +axiomatization where 1.9 1.10 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" 1.11