On 19/02/10 19:05 , Lu Zhao wrote: > I have a goal looks like the following
> `f x = f y` > I want to reduce it to > `x = y` > How can I do this, if it's doable? AP_TERM_TAC. If f is injective, you should add that fact to your simpset so that this transformation happens with simplification. Michael. ------------------------------------------------------------------------------ Download Intel® Parallel Studio Eval Try the new software tools for yourself. Speed compiling, find bugs proactively, and fine-tune applications for parallel performance. See why Intel Parallel Studio got high marks during beta. http://p.sf.net/sfu/intel-sw-dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
