# HG changeset patch
# User huffman
# Date 1215021177 -7200
# Node ID 0829a2c4b287b786ae362124caa163c9e7a7813a
# Parent  a487aa8925405c495fa7b6f8c6c171c8edb9d324
section -> subsection

diff -r a487aa892540 -r 0829a2c4b287 src/HOL/Complex/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Wed Jul 02 19:52:38 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Wed Jul 02 19:52:57 2008 +0200
@@ -9,7 +9,7 @@
 imports Univ_Poly Dense_Linear_Order Complex
 begin
 
-section {* Square root of complex numbers *}
+subsection {* Square root of complex numbers *}
 definition csqrt :: "complex \<Rightarrow> complex" where
 "csqrt z = (if Im z = 0 then
             if 0 \<le> Re z then Complex (sqrt(Re z)) 0
@@ -56,7 +56,7 @@
 qed
 
 
-section{* More lemmas about module of complex numbers *}
+subsection{* More lemmas about module of complex numbers *}
 
 lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
   by (induct n, auto)
@@ -108,7 +108,7 @@
 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
   using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
 
-section{* Basic lemmas about complex polynomials *}
+subsection{* Basic lemmas about complex polynomials *}
 
 lemma poly_bound_exists:
   shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
@@ -196,7 +196,7 @@
 qed
 
 
-section{* Some theorems about Sequences*}
+subsection{* Some theorems about Sequences*}
 text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
 
 lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
@@ -360,7 +360,7 @@
   thus ?case by arith
 qed
 
-section {* Fundamental theorem of algebra *}
+subsection {* Fundamental theorem of algebra *}
 lemma  unimodular_reduce_norm:
   assumes md: "cmod z = 1"
   shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
@@ -984,7 +984,7 @@
   ultimately show ?case by blast  
 qed simp
 
-section{* Nullstellenstatz, degrees and divisibility of polynomials *}
+subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
 
 lemma nullstellensatz_lemma:
   fixes p :: "complex list"