diff -r ce09935439b3 -r 2e0b7ca391dc src/Tools/isac/Knowledge/DiophantEq.thy --- a/src/Tools/isac/Knowledge/DiophantEq.thy Wed Aug 03 18:17:27 2022 +0200 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Aug 04 12:48:37 2022 +0200 @@ -33,7 +33,7 @@ (Try (Calculate ''TIMES''))) e_e)" method met_test_diophant : "Test/solve_diophant" = - \{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], + \{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify}\ Program: diophant_equation.simps Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"