diff -r 19f1f7066917 -r 5443079512ea src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 15:57:40 2010 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 16:51:37 2010 +0100
@@ -47,16 +47,16 @@
 section {* Constants *}
 
 definition
-  coeff :: "['a up, nat] => ('a::zero)" where
-  "coeff p n = Rep_UP p n"
+  coeff :: "['a up, nat] => ('a::zero)"
+  where "coeff p n = Rep_UP p n"
 
 definition
-  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70) where
-  "monom a n = Abs_UP (%i. if i=n then a else 0)"
+  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70)
+  where "monom a n = Abs_UP (%i. if i=n then a else 0)"
 
 definition
-  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70) where
-  "a *s p = Abs_UP (%i. a * Rep_UP p i)"
+  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70)
+  where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
 
 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
 proof -
@@ -132,7 +132,7 @@
 begin
 
 definition
-  up_mult_def:  "p * q = Abs_UP (%n::nat. setsum
+  up_mult_def: "p * q = Abs_UP (%n::nat. setsum
                      (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
 
 instance ..
@@ -149,7 +149,7 @@
                      THE x. a * x = 1 else 0)"
 
 definition
-  up_divide_def:  "(a :: 'a up) / b = a * inverse b"
+  up_divide_def: "(a :: 'a up) / b = a * inverse b"
 
 instance ..
 
@@ -482,8 +482,8 @@
 section {* The degree function *}
 
 definition
-  deg :: "('a::zero) up => nat" where
-  "deg p = (LEAST n. bound n (coeff p))"
+  deg :: "('a::zero) up => nat"
+  where "deg p = (LEAST n. bound n (coeff p))"
 
 lemma deg_aboveI:
   "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"