[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!


2010-07-01 
q.g. Xu


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