1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -903,18 +903,18 @@
     1.4       Try (Rewrite_Set ''rat_reduce_1''))) #>
     1.5     Try (Rewrite_Set ''discard_parentheses1''))
     1.6     term)"
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -    [MethodC.prep_input @{theory} "met_simp_rat" [] MethodC.id_empty
     1.9 -      (["simplification", "of_rationals"],
    1.10 -        [("#Given" ,["Term t_t"]),
    1.11 -          ("#Where" ,["t_t is_ratpolyexp"]),
    1.12 -          ("#Find"  ,["normalform n_n"])],
    1.13 -	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
    1.14 -	        prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty 
    1.15 -				    [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
    1.16 -				  crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
    1.17 -				  @{thm simplify.simps})]
    1.18 -\<close> ML \<open>
    1.19 +
    1.20 +
    1.21 +method met_simp_rat : "simplification/of_rationals" =
    1.22 +  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
    1.23 +    prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty 
    1.24 +      [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
    1.25 +    crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close>
    1.26 +  Program: simplify.simps
    1.27 +  Given: "Term t_t"
    1.28 +  Where: "t_t is_ratpolyexp"
    1.29 +  Find: "normalform n_n"
    1.30 +ML \<open>
    1.31  \<close> ML \<open>
    1.32  \<close>
    1.33  end