src/Tools/isac/Knowledge/DiophantEq.thy
changeset 59416 229e5c9cf78b
parent 59411 3e241a6938ce
child 59424 406681ebe781
     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                                                          " ^