src/HOL/Library/SCT_Misc.thy

 (*  Title:      HOL/Library/SCT_Misc.thy
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
+header ""
+
 theory SCT_Misc
 imports Main
 begin
 
 subsection {* Searching in lists *}

   by (induct l) auto
 
 lemma index_of_length:
   "(x \<in> set l) = (index_of l x < length l)"
   by (induct l) auto
+
 
 subsection {* Some reasoning tools *}
 
 lemma inc_induct[consumes 1]:
   assumes less: "i \<le> j"

   assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   shows "thesis"
   using prems
   by auto
 
-section {* Sequences *}
+
+subsection {* Sequences *}
 
 types
   'a sequence = "nat \<Rightarrow> 'a"
 
-subsection {* Increasing sequences *}
+
+subsubsection {* Increasing sequences *}
 
 definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
 where
   "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)"
 

     with increasing_weak have "s j \<le> s i" by simp
     with `s i < s j` show ?thesis by simp
   qed
 qed (simp add:increasing_strict)
 
-subsection {* Sections induced by an increasing sequence *}
+
+subsubsection {* Sections induced by an increasing sequence *}
 
 abbreviation
   "section s i == {s i ..< s (Suc i)}"
 
 definition