branch | decompose-isar |
changeset 42211 | 51c3c007d7fd |
parent 42197 | 7497ff20f1e8 |
child 42425 | da7fbace995b |
1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jul 26 16:50:27 2011 +0200 1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Wed Jul 27 09:30:15 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 -axiomatization where 1.8 +axioms(*axiomatization where*) 1.9 1.10 int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))" 1.11