equal
deleted
inserted
replaced
79 |
79 |
80 (*WN080222:*) |
80 (*WN080222:*) |
81 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_")) |
81 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_")) |
82 add a new c to a term or a fun-equation; |
82 add a new c to a term or a fun-equation; |
83 this is _not in_ the term, because only applied to _whole_ term*) |
83 this is _not in_ the term, because only applied to _whole_ term*) |
84 fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) = |
84 fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:Proof.context) = |
85 let val p' = case p of |
85 let val p' = case p of |
86 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh => |
86 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh => |
87 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh) |
87 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh) |
88 | p => TermC.mk_add p (new_c p) |
88 | p => TermC.mk_add p (new_c p) |
89 in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p', |
89 in SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term p', |