1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -147,18 +147,15 @@
     1.4  ML \<open>
     1.5  Check_Unique.on := false; (*WN120307 REMOVE after editing*)
     1.6  \<close>
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_simp_rat_partfrac" [] Problem.id_empty
     1.9 -      (["partial_fraction", "rational", "simplification"],
    1.10 -        [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
    1.11 -          (* TODO: call this sub-problem with appropriate functionTerm: 
    1.12 -            leading coefficient of the denominator is 1: to be checked here! and..
    1.13 -            ("#Where" ,["((get_numerator t_t) has_degree_in v_v) < 
    1.14 -               ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
    1.15 -          ("#Find"  ,["decomposedFunction p_p'''"])],
    1.16 -        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)], 
    1.17 -        NONE, 
    1.18 -        [["simplification", "of_rationals", "to_partial_fraction"]]))]\<close>
    1.19 +problem pbl_simp_rat_partfrac : "partial_fraction/rational/simplification" =
    1.20 +  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_ TODO*)]\<close>
    1.21 +  Method: "simplification/of_rationals/to_partial_fraction"
    1.22 +  Given: "functionTerm t_t" "solveFor v_v"
    1.23 +  (* TODO: call this sub-problem with appropriate functionTerm: 
    1.24 +    leading coefficient of the denominator is 1: to be checked here! and..
    1.25 +  Where: "((get_numerator t_t) has_degree_in v_v) < 
    1.26 +       ((get_denominator t_t) has_degree_in v_v)" TODO*)
    1.27 +  Find: "decomposedFunction p_p'''"
    1.28  
    1.29  subsection \<open>MethodC\<close>
    1.30  text \<open>rule set for functions called in the Program\<close>