245 val (Form f, tac, asms) = pt_extract (pt, p); |
245 val (Form f, tac, asms) = pt_extract (pt, p); |
246 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso |
246 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso |
247 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^ |
247 terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^ |
248 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^ |
248 "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^ |
249 "B is_polyexp,A is_polyexp," ^ |
249 "B is_polyexp,A is_polyexp," ^ |
250 "~ matches (?a = 0) (3 = 3 * A / 4) | ~ lhs (3 = 3 * A / 4) is_poly_in A," ^ |
250 "<not> matches (?a = 0) (3 = 3 * A / 4) | <not> lhs (3 = 3 * A / 4) is_poly_in A," ^ |
251 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^ |
251 "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^ |
252 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^ |
252 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^ |
253 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]" |
253 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]" |
254 then case tac of NONE => () |
254 then case tac of NONE => () |
255 | _ => error "autoCalculate for met_partial_fraction changed: final result 1" |
255 | _ => error "autoCalculate for met_partial_fraction changed: final result 1" |