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"],