257 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
257 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = |
258 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
258 ["Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
259 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", |
259 "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", |
260 (*this is new since ThmC.numerals_to_Free.-----\\*) |
260 (*this is new since ThmC.numerals_to_Free.-----\\*) |
261 "Calculate PLUS"] |
261 "Calculate PLUS"] |
262 then () else error "specific_from_prog ([1], Res) 1 CHANGED"; (*GOON*) |
262 then () else error "specific_from_prog ([1], Res) 1 CHANGED"; |
263 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p); |
263 (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p); |
264 |
264 |
265 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [ |
265 (*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [ |
266 "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", |
266 "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", |
267 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |
267 "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_num; ?m is_num\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")", |