--- 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"