1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 18:59:30 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 20:38:23 2021 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  theory DiophantEq imports Base_Tools Equation Test
     1.5  begin
     1.6  
     1.7 -axiomatization where
     1.8 -  int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
     1.9 +lemma int_isolate_add : "(bdv + a = b) = (bdv = b +  -1 * (a::int))"
    1.10 +  by auto
    1.11  
    1.12  text \<open>problemclass for the usecase\<close>
    1.13