--- a/src/HOL/Algebra/UnivPoly.thy Sun Mar 08 17:05:43 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Mar 08 17:19:15 2009 +0100
@@ -190,7 +190,7 @@
context UP
begin
-text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
+text {*Temporarily declare @{thm P_def} as simp rule.*}
declare P_def [simp]
@@ -638,8 +638,8 @@
}
qed
-text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"}
- and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
+text{*The following corollary follows from lemmas @{thm "monom_one_Suc"}
+ and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..