1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -33,8 +33,8 @@
     1.4      (Try (Calculate ''TIMES''))) e_e)"
     1.5  
     1.6  method met_test_diophant : "Test/solve_diophant" =
     1.7 -  \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
     1.8 -    crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
     1.9 +  \<open>{rew_ord = "Rewrite_Ord.id_empty", rls' = tval_rls, prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, calc = [],
    1.10 +    crls = tval_rls, errpats = [], rew_rls = Test_simplify}\<close>
    1.11    Program: diophant_equation.simps
    1.12    Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
    1.13  (*                                  TODO: drop ^^^^^*)