# HG changeset patch
# User wenzelm
# Date 1230838083 -3600
# Node ID 11045b88af1a560026d1330cf4181bb24ed138b6
# Parent  d3cc5398bad5f42e42afda3b26ccfbf24bda3e41
avoid implicit prems -- tuned proofs;

diff -r d3cc5398bad5 -r 11045b88af1a src/HOL/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Jan 01 17:47:12 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Jan 01 20:28:03 2009 +0100
@@ -16,7 +16,7 @@
 
 lemma csqrt[algebra]: "csqrt z ^ 2 = z"
 proof-
-  obtain x y where xy: "z = Complex x y" by (cases z, simp_all)
+  obtain x y where xy: "z = Complex x y" by (cases z)
   {assume y0: "y = 0"
     {assume x0: "x \<ge> 0" 
       then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
diff -r d3cc5398bad5 -r 11045b88af1a src/HOL/Univ_Poly.thy
--- a/src/HOL/Univ_Poly.thy	Thu Jan 01 17:47:12 2009 +0100
+++ b/src/HOL/Univ_Poly.thy	Thu Jan 01 20:28:03 2009 +0100
@@ -2,7 +2,7 @@
     Author:      Amine Chaieb
 *)
 
-header{*Univariate Polynomials*}
+header {* Univariate Polynomials *}
 
 theory Univ_Poly
 imports Plain List
@@ -368,12 +368,13 @@
   "\<not> (finite (UNIV:: 'a set))" 
 proof
   assume F: "finite (UNIV :: 'a set)"
-  have th0: "of_nat ` UNIV \<subseteq> UNIV" by simp
-  from finite_subset[OF th0] have th: "finite (of_nat ` UNIV :: 'a set)" .
-  have th': "inj_on (of_nat::nat \<Rightarrow> 'a) (UNIV)"
-    unfolding inj_on_def by auto
-  from finite_imageD[OF th th'] UNIV_nat_infinite 
-  show False by blast
+  have "finite (UNIV :: nat set)"
+  proof (rule finite_imageD)
+    have "of_nat ` UNIV \<subseteq> UNIV" by simp
+    then show "finite (of_nat ` UNIV :: 'a set)" using F by (rule finite_subset)
+    show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: inj_on_def)
+  qed
+  with UNIV_nat_infinite show False ..
 qed
 
 lemma (in idom_char_0) poly_roots_finite: "(poly p \<noteq> poly []) = 
@@ -580,8 +581,8 @@
 next
   case (Suc n p)
   {assume p0: "poly p a = 0"
-    from Suc.prems have h: "length p = Suc n" "poly p \<noteq> poly []" by blast
-    hence pN: "p \<noteq> []" by - (rule ccontr, simp)
+    from Suc.prems have h: "length p = Suc n" "poly p \<noteq> poly []" by auto
+    hence pN: "p \<noteq> []" by auto
     from p0[unfolded poly_linear_divides] pN  obtain q where 
       q: "p = [-a, 1] *** q" by blast
     from q h p0 have qh: "length q = n" "poly q \<noteq> poly []"