1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Sun Mar 25 13:59:57 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Mon Mar 26 07:28:39 2018 +0200
1.3 @@ -26,7 +26,7 @@
1.4 (* TODO: drop ^^^^^*)
1.5 ("#Where" ,[]),
1.6 ("#Find" ,["boolTestFind s_s"])],
1.7 - Celem.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
1.8 + Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
1.9
1.10 text {*method solving the usecase*}
1.11 setup {* KEStore_Elems.add_mets
1.12 @@ -36,7 +36,7 @@
1.13 (* TODO: drop ^^^^^*)
1.14 ("#Where" ,[]),
1.15 ("#Find" ,["boolTestFind s_s"])],
1.16 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Celem.e_rls, prls = Celem.e_rls, calc = [],
1.17 + {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [],
1.18 crls = tval_rls, errpats = [], nrls = Test_simplify},
1.19 "Script Diophant_equation (e_e::bool) (v_v::int)= " ^
1.20 "(Repeat " ^