1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -38,22 +38,21 @@
     1.4  	       [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")];
     1.5  \<close>
     1.6  rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_equ" [] Problem.id_empty
     1.9 -      (["equation"],
    1.10 -        [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.11 -          ("#Where" ,["matches (?a = ?b) e_e"]),
    1.12 -          ("#Find"  ,["solutions v_v'i'"])],
    1.13 -        Rule_Set.append_rules "equation_prls" Rule_Set.empty
    1.14 -          [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")],
    1.15 -        SOME "solve (e_e::bool, v_v)", [])),
    1.16 -    (Problem.prep_input @{theory} "pbl_equ_univ" [] Problem.id_empty
    1.17 -      (["univariate", "equation"],
    1.18 -        [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.19 -          ("#Where" ,["matches (?a = ?b) e_e"]),
    1.20 -          ("#Find"  ,["solutions v_v'i'"])],
    1.21 -        univariate_equation_prls, SOME "solve (e_e::bool, v_v)", []))]\<close>
    1.22  
    1.23 +problem pbl_equ : "equation" =
    1.24 +  \<open>Rule_Set.append_rules "equation_prls" Rule_Set.empty
    1.25 +    [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches "")]\<close>
    1.26 +  CAS: "solve (e_e::bool, v_v)"
    1.27 +  Given: "equality e_e" "solveFor v_v"
    1.28 +  Where: "matches (?a = ?b) e_e"
    1.29 +  Find: "solutions v_v'i'"
    1.30 +
    1.31 +problem pbl_equ_univ : "univariate/equation" =
    1.32 +  \<open>univariate_equation_prls\<close>
    1.33 +  CAS: "solve (e_e::bool, v_v)"
    1.34 +  Given: "equality e_e" "solveFor v_v"
    1.35 +  Where: "matches (?a = ?b) e_e"
    1.36 +  Find: "solutions v_v'i'"
    1.37  
    1.38  ML\<open>
    1.39  (*.function for handling the cas-input "solve (x+1=2, x)":