equal
deleted
inserted
replaced
100 val cc = new_c term; |
100 val cc = new_c term; |
101 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???"; |
101 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???"; |
102 |
102 |
103 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy; |
103 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy; |
104 "####1###################################################"; |
104 "####1###################################################"; |
105 term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +"; |
105 term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "Groups.plus_class.plus"; |
106 "####2###################################################"; |
106 "####2###################################################"; |
107 |
107 |
108 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then () |
108 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then () |
109 else raise error "intergrate.sml: diff. eval_add_new_c"; |
109 else raise error "intergrate.sml: diff. eval_add_new_c"; |
110 |
110 |