equal
deleted
inserted
replaced
100 val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term ctxt; |
100 val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term ctxt; |
101 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then () |
101 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then () |
102 else error "intergrate.sml: diff. eval_add_new_c"; |
102 else error "intergrate.sml: diff. eval_add_new_c"; |
103 |
103 |
104 val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_"); |
104 val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_"); |
105 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term; |
105 val SOME (thmstr, thm) = adhoc_thm1_ @{context} cc term; |
106 |
106 |
107 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term; |
107 val SOME (t',_) = rewrite_set_ ctxt true add_new_c term; |
108 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then () |
108 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then () |
109 else error "intergrate.sml: diff. rewrite_set add_new_c 1"; |
109 else error "intergrate.sml: diff. rewrite_set add_new_c 1"; |
110 |
110 |