[isabelle] 回复: Re: about ring_simps
thanks for your reply and giving a good solution.
As to Emacs command "proof-find-theorems" you have mentioned, I have tried the pattern (_+_)^2
the following message answers me.
*** Outer syntax error: keyword ")" expected,
*** but symbolic identifier _+_ was found
the pattern "(_+_)^2" works fine.
what's the play about the quotation marks "" ?
thank you again.
From: Alex Katovsky
Date: 2010-07-01 15:54:19
Subject: Re: [isabelle] about ring_simps
If you replace "ring_simps" by "power2_sum power2_diff" then it works. There are a few more problems with the file (I have attached one that compiles). In general, if you are looking for a theorem, you can search for it by using the Emacs command "proof-find-theorems", which is bound to the key sequence "C-c C-f". In this case, you would search for
Find theorems containing: "(_+_)^2"
And the search returns what we are looking for in this case.
On 07/01/2010 02:42 AM, 许庆国 wrote:
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and