src/Tools/isac/Knowledge/DiophantEq.thy
branchdecompose-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