src/HOL/Algebra/UnivPoly.thy
changeset 30363 9b8d9b6ef803
parent 29246 3593802c9cf1
child 30729 461ee3e49ad3
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 08 17:05:43 2009 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Mar 08 17:19:15 2009 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  context UP
     1.5  begin
     1.6  
     1.7 -text {*Temporarily declare @{thm [locale=UP] P_def} as simp rule.*}
     1.8 +text {*Temporarily declare @{thm P_def} as simp rule.*}
     1.9  
    1.10  declare P_def [simp]
    1.11  
    1.12 @@ -638,8 +638,8 @@
    1.13    }
    1.14  qed
    1.15  
    1.16 -text{*The following corollary follows from lemmas @{thm [locale=UP_ring] "monom_one_Suc"} 
    1.17 -  and @{thm [locale=UP_ring] "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
    1.18 +text{*The following corollary follows from lemmas @{thm "monom_one_Suc"} 
    1.19 +  and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}*}
    1.20  
    1.21  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"
    1.22    unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..