wordsLib.WORD_ARITH_EQ_ss doesn't do very much. It simply performs the conversion
x = y |-> x - y = 0w but it does not simplify "x - y". It is expected to be used in combination with wordsLib.WORD_ARITH_ss, which is included in the stateful simpset srw_ss() but not in std_ss. The simpsets wordsLib.WORD_ARITH_EQ_ss wordsLib.WORD_BIT_EQ_ss wordsLib.WORD_EXTRACT_ss are not included in the stateful simpset, but they can help in some situations. Anthony. On 13 Dec 2009, at 04:06, Lu Zhao wrote: > Hi Anthony and Magnus, > > Thank you very much for the solution. > > I have a question on srw_ss(). Before sending the email for help, I used > > SIMP_TAC (std_ss++WORD_ARITH_EQ_ss) [] > > but it didn't work. Why does srw_ss() work and std_ss not? In what situations > should I use srw_ss()? > > Lu ------------------------------------------------------------------------------ Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
