Re: [Hol-info] How to remove a same function in a goal

2010-02-19 Thread Michael Norrish
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.

[Hol-info] How to remove a same function in a goal

2010-02-19 Thread Lu Zhao
Hi, 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? Thanks. Lu -- Download IntelĀ® Parallel Studio Eval Try the new software tools for yourself. Spe