src/HOL/Algebra/UnivPoly.thy
changeset 30729 461ee3e49ad3
parent 30363 9b8d9b6ef803
child 32436 10cd49e0c067
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -1886,7 +1886,7 @@
     1.4    "UP INTEG"} globally.
     1.5  *}
     1.6  
     1.7 -interpretation INTEG!: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
     1.8 +interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
     1.9    using INTEG_id_eval by simp_all
    1.10  
    1.11  lemma INTEG_closed [intro, simp]: