[isabelle] about ring_simps

Hello everyone:

    I am learning Isabelle through the the website: http://isabelle.in.tum.de/coursematerial/PSV2009-1/index.html  
  When I am tring to check the file thttp://isabelle.in.tum.de/coursematerial/PSV2009-1/session78/Demo2.thy.
  the following message shows:
    *** Unknown fact "ring_simps"
	*** At command "by".
in the process of proving              
  lemma fixes a :: int shows "(a+b)2 <= 2*(a2 + b2)" 
  also have "(a+b)2 £ a2 + b2 + 2*a*b"  by(simp add:numeral_2_eq_2 ring_simps

Now my Isabells's version is Isabelle 2009-2.

How to correct this error? 
thanks a lot in advance!

q.g. Xu

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.