--- a/src/HOL/Algebra/UnivPoly.thy Thu Nov 23 20:33:42 2006 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Thu Nov 23 20:34:21 2006 +0100
@@ -1161,8 +1161,9 @@
text {* Further properties of the evaluation homomorphism. *}
-(* The following lemma could be proved in UP\_cring with the additional
- assumption that h is closed. *)
+text {*
+ The following lemma could be proved in @{text UP_cring} with the additional
+ assumption that @{text h} is closed. *}
lemma (in UP_pre_univ_prop) eval_const:
"[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"