src/Tools/isac/Knowledge/Equation.thy
changeset 59603 30cd47104ad7
parent 59592 99c8d2ff63eb
child 59618 80efccb7e5c1
     1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Thu Aug 29 13:52:47 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Tue Sep 03 12:40:27 2019 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  val univariate_equation_prls = 
     1.6      Rule.append_rls "univariate_equation_prls" Rule.e_rls 
     1.7 -	       [Rule.Calc ("Tools.matches", Tools.eval_matches "")];
     1.8 +	       [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
     1.9  \<close>
    1.10  setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
    1.11    (Context.theory_name @{theory}, LTool.prep_rls @{theory} univariate_equation_prls))]\<close>
    1.12 @@ -48,7 +48,7 @@
    1.13          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.14            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.15            ("#Find"  ,["solutions v_v'i'"])],
    1.16 -        Rule.append_rls "equation_prls" Rule.e_rls  [Rule.Calc ("Tools.matches", Tools.eval_matches "")],
    1.17 +        Rule.append_rls "equation_prls" Rule.e_rls  [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
    1.18          SOME "solve (e_e::bool, v_v)", [])),
    1.19      (Specify.prep_pbt thy "pbl_equ_univ" [] Celem.e_pblID
    1.20        (["univariate","equation"],