equal
deleted
inserted
replaced
105 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy; |
105 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy; |
106 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then () |
106 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then () |
107 else error "intergrate.sml: diff. eval_add_new_c"; |
107 else error "intergrate.sml: diff. eval_add_new_c"; |
108 |
108 |
109 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"); |
109 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"); |
110 val SOME (thmstr, thm) = get_calculation1_ thy cc term; |
110 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term; |
111 |
111 |
112 val SOME (t',_) = rewrite_set_ thy true add_new_c term; |
112 val SOME (t',_) = rewrite_set_ thy true add_new_c term; |
113 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then () |
113 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then () |
114 else error "intergrate.sml: diff. rewrite_set add_new_c 1"; |
114 else error "intergrate.sml: diff. rewrite_set add_new_c 1"; |
115 |
115 |