Re: [isabelle] about ring_simps



Please use algebra_simps now; ring_simps and a number of other special
sets of algebraic simplification rules have been combined into
algebra_simps.

I will update the slides, thanks.
Tobias

许庆国 wrote:
> 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.