--- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Aug 28 18:52:41 2009 +0200
@@ -563,11 +563,7 @@
lemma deg_add [simp]:
"deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
- case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD)
-next
- case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
+by (rule deg_aboveI) (simp add: deg_aboveD)
lemma deg_monom_ring:
"deg (monom a n::'a::ring up) <= n"