1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -875,14 +875,14 @@
     1.4    cancel_p_rls = cancel_p_rls
     1.5  
     1.6  section \<open>A problem for simplification of rationals\<close>
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_simp_rat" [] Problem.id_empty
     1.9 -      (["rational", "simplification"],
    1.10 -        [("#Given" ,["Term t_t"]),
    1.11 -          ("#Where" ,["t_t is_ratpolyexp"]),
    1.12 -          ("#Find"  ,["normalform n_n"])],
    1.13 -        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.14 -        SOME "Simplify t_t", [["simplification", "of_rationals"]]))]\<close>
    1.15 +
    1.16 +problem pbl_simp_rat : "rational/simplification" =
    1.17 +  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.18 +  Method: "simplification/of_rationals"
    1.19 +  CAS: "Simplify t_t"
    1.20 +  Given: "Term t_t"
    1.21 +  Where: "t_t is_ratpolyexp"
    1.22 +  Find: "normalform n_n"
    1.23  
    1.24  section \<open>A methods for simplification of rationals\<close>
    1.25  (*WN061025 this methods script is copied from (auto-generated) script