src/Tools/isac/Knowledge/Equation.thy
changeset 59773 d88bb023c380
parent 59618 80efccb7e5c1
child 59850 f3cac3053e7b
     1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Fri Jan 17 13:14:11 2020 +0100
     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 ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
     1.8 +	       [Rule.Num_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}, Auto_Prog.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 ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
    1.17 +        Rule.append_rls "equation_prls" Rule.e_rls  [Rule.Num_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"],