src/HOL/Algebra/UnivPoly.thy
changeset 21502 7f3ea2b3bab6
parent 20432 07ec57376051
child 22931 11cc1ccad58e
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Nov 23 20:33:42 2006 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Nov 23 20:34:21 2006 +0100
     1.3 @@ -1161,8 +1161,9 @@
     1.4  
     1.5  text {* Further properties of the evaluation homomorphism. *}
     1.6  
     1.7 -(* The following lemma could be proved in UP\_cring with the additional
     1.8 -   assumption that h is closed. *)
     1.9 +text {*
    1.10 +  The following lemma could be proved in @{text UP_cring} with the additional
    1.11 +  assumption that @{text h} is closed. *}
    1.12  
    1.13  lemma (in UP_pre_univ_prop) eval_const:
    1.14    "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"