252 |
252 |
253 (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f |
253 (*+*)val Test_Out.FormKF "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12" = f |
254 |
254 |
255 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) |
255 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "fasse_zusammen"*) |
256 |
256 |
|
257 (*+*)val Test_Out.FormKF "??.empty" = f; |
|
258 (** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** ) |
257 (*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f; |
259 (*+*)val Test_Out.FormKF "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g" = f; |
258 |
260 |
259 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
261 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
260 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
262 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
261 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", |
263 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", |
375 UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]" |
377 UnparseC.terms asm = "[\"4 kleiner 6\",\"6 ist_monom\"]" |
376 then () else error "locate_input_tactic Helpless, but applicable CHANGED"; |
378 then () else error "locate_input_tactic Helpless, but applicable CHANGED"; |
377 ( *\----- original before child of 7e314dd233fd -------------------------------------------------/*) |
379 ( *\----- original before child of 7e314dd233fd -------------------------------------------------/*) |
378 |
380 |
379 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = Rewrite_Set "fasse_zusammen"*) |
381 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt'''''; (*nxt = Rewrite_Set "fasse_zusammen"*) |
|
382 ( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **) |
380 |
383 |
381 |
384 |
382 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |
385 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |
383 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |
386 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |
384 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |
387 "----------- re-build: fun find_next_step, mini ------------------------------------------------"; |