510 \<close> ML \<open> |
510 \<close> ML \<open> |
511 f |
511 f |
512 \<close> ML \<open> |
512 \<close> ML \<open> |
513 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) |
513 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ordne_alphabetisch"*) |
514 \<close> ML \<open> |
514 \<close> ML \<open> |
515 val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f |
515 (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f |
516 \<close> ML \<open> |
516 \<close> ML \<open> |
517 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) |
517 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) |
518 |
518 |
519 \<close> ML \<open> |
519 \<close> ML \<open> |
520 f |
520 (*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f |
521 \<close> ML \<open> |
521 \<close> ML \<open> |
|
522 \<close> ML \<open> (*GOON*) |
522 map Tactic.input_to_string (specific_from_prog pt p) |
523 map Tactic.input_to_string (specific_from_prog pt p) |
523 \<close> ML \<open> |
524 \<close> ML \<open> |
524 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
525 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
525 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
526 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
526 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"] |
527 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")"] |
969 |
970 |
970 ML_file "Knowledge/delete.sml" |
971 ML_file "Knowledge/delete.sml" |
971 ML_file "Knowledge/descript.sml" |
972 ML_file "Knowledge/descript.sml" |
972 ML_file "Knowledge/simplify.sml" |
973 ML_file "Knowledge/simplify.sml" |
973 ML_file "Knowledge/poly.sml" |
974 ML_file "Knowledge/poly.sml" |
|
975 ML \<open> |
|
976 \<close> ML \<open> |
|
977 \<close> ML \<open> |
|
978 \<close> ML \<open> |
|
979 \<close> ML \<open> |
|
980 \<close> ML \<open> |
|
981 \<close> ML \<open> |
|
982 \<close> ML \<open> |
|
983 \<close> ML \<open> |
|
984 \<close> ML \<open> |
|
985 \<close> ML \<open> |
|
986 \<close> |
974 ML_file "Knowledge/gcd_poly_ml.sml" |
987 ML_file "Knowledge/gcd_poly_ml.sml" |
975 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) |
988 ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*) |
976 ML_file "Knowledge/rational.sml" (*Test_Isac_Short*) |
989 ML_file "Knowledge/rational.sml" (*Test_Isac_Short*) |
977 ML_file "Knowledge/equation.sml" |
990 ML_file "Knowledge/equation.sml" |
978 ML_file "Knowledge/root.sml" |
991 ML_file "Knowledge/root.sml" |