equal
deleted
inserted
replaced
829 |
829 |
830 section \<open>A problem for simplification of rationals\<close> |
830 section \<open>A problem for simplification of rationals\<close> |
831 |
831 |
832 problem pbl_simp_rat : "rational/simplification" = |
832 problem pbl_simp_rat : "rational/simplification" = |
833 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close> |
833 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close> |
834 Method: "simplification/of_rationals" |
834 Method_Ref: "simplification/of_rationals" |
835 CAS: "Simplify t_t" |
835 CAS: "Simplify t_t" |
836 Given: "Term t_t" |
836 Given: "Term t_t" |
837 Where: "t_t is_ratpolyexp" |
837 Where: "t_t is_ratpolyexp" |
838 Find: "normalform n_n" |
838 Find: "normalform n_n" |
839 |
839 |