diff -r e965391e2864 -r cf152ff55d16 src/HOL/Library/SCT_Theorem.thy
--- a/src/HOL/Library/SCT_Theorem.thy	Fri Apr 13 21:26:34 2007 +0200
+++ b/src/HOL/Library/SCT_Theorem.thy	Fri Apr 13 21:26:35 2007 +0200
@@ -3,11 +3,13 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
+header ""
+
 theory SCT_Theorem
 imports Main Ramsey SCT_Misc SCT_Definition
 begin
 
-section {* The size change criterion SCT *}
+subsection {* The size change criterion SCT *}
 
 definition is_thread :: "nat \<Rightarrow> nat sequence \<Rightarrow> (nat, scg) ipath \<Rightarrow> bool"
 where
@@ -33,7 +35,8 @@
   "has_desc_fth p i j n m = 
   (\<exists>\<theta>. is_desc_fthread \<theta> p i j \<and> \<theta> i = n \<and> \<theta> j = m)"
 
-section {* Bounded graphs and threads *}
+
+subsection {* Bounded graphs and threads *}
 
 definition 
   "bounded_scg (P::nat) (G::scg) = 
@@ -325,9 +328,7 @@
 qed
 
 
-
-section {* Contraction and more *}
-
+subsection {* Contraction and more *}
 
 abbreviation 
   "pdesc P == (fst P, prod P, end_node P)"
@@ -342,8 +343,6 @@
   by (auto intro:sub_path_is_path[of "\<A>" p i j] simp:sub_path_def)
 
 
-
-
 lemma combine_fthreads: 
   assumes range: "i < j" "j \<le> k"
   shows 
@@ -657,7 +656,7 @@
   by (auto simp:Lemma7a increasing_weak contract_def)
 
 
-subsection {* Connecting threads *}
+subsubsection {* Connecting threads *}
 
 definition
   "connect s \<theta>s = (\<lambda>k. \<theta>s (section_of s k) k)"
@@ -685,7 +684,6 @@
 qed
 
 
-
 lemma connect_threads:
   assumes [simp]: "increasing s"
   assumes connected: "\<theta>s i (s (Suc i)) = \<theta>s (Suc i) (s (Suc i))"
@@ -889,7 +887,7 @@
   assume "?A"
   then obtain \<theta> n 
     where fr: "\<forall>i\<ge>n. eqlat p \<theta> i" 
-    and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
+      and ds: "\<exists>\<^sub>\<infinity>i. descat p \<theta> i"
     unfolding is_desc_thread_def 
     by auto
 
@@ -903,18 +901,18 @@
     proof (intro allI impI)
       fix i assume "n \<le> i"
       also have "i \<le> s i" 
-	    using increasing_inc by auto
+	using increasing_inc by auto
       finally have "n \<le> s i" .
 
       with fr have "is_fthread \<theta> p (s i) (s (Suc i))"
-	    unfolding is_fthread_def by auto
+	unfolding is_fthread_def by auto
       hence "has_fth p (s i) (s (Suc i)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
-	    unfolding has_fth_def by auto
+	unfolding has_fth_def by auto
       with less_imp_le[OF increasing_strict]
       have "eql (prod (p\<langle>s i,s (Suc i)\<rangle>)) (\<theta> (s i)) (\<theta> (s (Suc i)))"
-	    by (simp add:Lemma7a)
+	by (simp add:Lemma7a)
       thus "eqlat (contract s p) ?c\<theta> i" unfolding contract_def
-	    by auto
+	by auto
     qed
 
     show "\<exists>\<^sub>\<infinity>i. descat (contract s p) ?c\<theta> i"
@@ -924,57 +922,56 @@
 
       let ?K = "section_of s (max (s (Suc i)) n)"
       from `\<exists>\<^sub>\<infinity>i. descat p \<theta> i` obtain j
-	    where "s (Suc ?K) < j" "descat p \<theta> j"
-	    unfolding INF_nat by blast
+	  where "s (Suc ?K) < j" "descat p \<theta> j"
+	unfolding INF_nat by blast
       
       let ?L = "section_of s j"
       {
-	    fix x assume r: "x \<in> section s ?L"
-
-	    have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
+	fix x assume r: "x \<in> section s ?L"
+	
+	have e1: "max (s (Suc i)) n < s (Suc ?K)" by (rule section_of2)
         note `s (Suc ?K) < j`
         also have "j < s (Suc ?L)"
           by (rule section_of2)
         finally have "Suc ?K \<le> ?L"
           by (simp add:increasing_bij)          
-	    with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
-	    with e1 r have "max (s (Suc i)) n < x" by simp
+	with increasing_weak have "s (Suc ?K) \<le> s ?L" by simp
+	with e1 r have "max (s (Suc i)) n < x" by simp
         
-	    hence "(s (Suc i)) < x" "n < x" by auto
+	hence "(s (Suc i)) < x" "n < x" by auto
       }
       note range_est = this
       
       have "is_desc_fthread \<theta> p (s ?L) (s (Suc ?L))"
-	    unfolding is_desc_fthread_def is_fthread_def
+	unfolding is_desc_fthread_def is_fthread_def
       proof
-	    show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
+	show "\<forall>m\<in>section s ?L. eqlat p \<theta> m"
         proof 
           fix m assume "m\<in>section s ?L"
           with range_est(2) have "n < m" . 
           with fr show "eqlat p \<theta> m" by simp
         qed
-        
 
         from in_section_of inc less_imp_le[OF `s (Suc ?K) < j`]
-	    have "j \<in> section s ?L" .
+	have "j \<in> section s ?L" .
 
-	    with `descat p \<theta> j`
-	    show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
+	with `descat p \<theta> j`
+	show "\<exists>m\<in>section s ?L. descat p \<theta> m" ..
       qed
       
       with less_imp_le[OF increasing_strict]
       have a: "descat (contract s p) ?c\<theta> ?L"
-	    unfolding contract_def Lemma7b[symmetric]
-	    by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
+	unfolding contract_def Lemma7b[symmetric]
+	by (auto simp:Lemma7b[symmetric] has_desc_fth_def)
       
       have "i < ?L"
       proof (rule classical)
-	    assume "\<not> i < ?L" 
-	    hence "s ?L < s (Suc i)" 
+	assume "\<not> i < ?L" 
+	hence "s ?L < s (Suc i)" 
           by (simp add:increasing_bij)
-	    also have "\<dots> < s ?L"
-	      by (rule range_est(1)) (simp add:increasing_strict)
-	    finally show ?thesis .
+	also have "\<dots> < s ?L"
+	  by (rule range_est(1)) (simp add:increasing_strict)
+	finally show ?thesis .
       qed
       with a show "\<exists>l. i < l \<and> descat (contract s p) ?c\<theta> l"
         by blast
@@ -994,7 +991,7 @@
           (\<lambda>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))
                   \<and> \<theta>s i (s i) = \<theta> i 
                   \<and> \<theta>s i (s (Suc i)) = \<theta> (Suc i))" 
-    (is "desc ?alw ?inf") 
+      (is "desc ?alw ?inf") 
     by blast
 
   then obtain n where fr: "\<forall>i\<ge>n. ?alw i" by blast
@@ -1004,8 +1001,8 @@
   let ?j\<theta> = "connect s \<theta>s"
   
   from fr ths_spec have ths_spec2:
-    "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
-    "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
+      "\<And>i. i > n \<Longrightarrow> is_fthread (\<theta>s i) p (s i) (s (Suc i))"
+      "\<exists>\<^sub>\<infinity>i. is_desc_fthread (\<theta>s i) p (s i) (s (Suc i))"
     by (auto intro:INF_mono)
   
   have p1: "\<And>i. i > n \<Longrightarrow> is_fthread ?j\<theta> p (s i) (s (Suc i))"
@@ -1027,7 +1024,6 @@
 qed
 
 
-
 lemma repeated_edge:
   assumes "\<And>i. i > n \<Longrightarrow> dsc (snd (p i)) k k"
   shows "is_desc_thread (\<lambda>i. k) p"
@@ -1050,9 +1046,7 @@
   by auto
 
 
-
-section {* Ramsey's Theorem *}
-
+subsection {* Ramsey's Theorem *}
 
 definition 
   "set2pair S = (THE (x,y). x < y \<and> S = {x,y})"
@@ -1176,8 +1170,7 @@
 qed
 
 
-section {* Main Result *}
-
+subsection {* Main Result *}
 
 theorem LJA_Theorem4: 
   assumes "bounded_acg P \<A>"
@@ -1383,7 +1376,6 @@
 qed
 
 
-
 lemma LJA_apply:
   assumes fin: "finite_acg A"
   assumes "SCT' A"