901 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #> |
901 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #> |
902 Try (Rewrite_Set ''cancel_p_rls'') #> |
902 Try (Rewrite_Set ''cancel_p_rls'') #> |
903 Try (Rewrite_Set ''rat_reduce_1''))) #> |
903 Try (Rewrite_Set ''rat_reduce_1''))) #> |
904 Try (Rewrite_Set ''discard_parentheses1'')) |
904 Try (Rewrite_Set ''discard_parentheses1'')) |
905 term)" |
905 term)" |
906 setup \<open>KEStore_Elems.add_mets |
906 |
907 [MethodC.prep_input @{theory} "met_simp_rat" [] MethodC.id_empty |
907 |
908 (["simplification", "of_rationals"], |
908 method met_simp_rat : "simplification/of_rationals" = |
909 [("#Given" ,["Term t_t"]), |
909 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, |
910 ("#Where" ,["t_t is_ratpolyexp"]), |
910 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty |
911 ("#Find" ,["normalform n_n"])], |
911 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")], |
912 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, |
912 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close> |
913 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty |
913 Program: simplify.simps |
914 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")], |
914 Given: "Term t_t" |
915 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}, |
915 Where: "t_t is_ratpolyexp" |
916 @{thm simplify.simps})] |
916 Find: "normalform n_n" |
|
917 ML \<open> |
917 \<close> ML \<open> |
918 \<close> ML \<open> |
918 \<close> ML \<open> |
|
919 \<close> |
919 \<close> |
920 end |
920 end |