summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"