diff -r d9b53c240c5f -r 4f5f29fd0af9 src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 18:59:30 2021 +0200
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sat Aug 14 20:38:23 2021 +0200
@@ -8,8 +8,8 @@
 theory DiophantEq imports Base_Tools Equation Test
 begin
 
-axiomatization where
-  int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"
+lemma int_isolate_add : "(bdv + a = b) = (bdv = b +  -1 * (a::int))"
+  by auto
 
 text \<open>problemclass for the usecase\<close>