diff -r 9c3377b133c0 -r d982f98e0f0d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Nov 03 01:33:33 2001 +0100
+++ b/src/HOL/Set.thy	Sat Nov 03 01:33:54 2001 +0100
@@ -515,7 +515,7 @@
   by (blast elim: equalityE)
 
 
-section {* The Powerset operator -- Pow *}
+subsubsection {* The Powerset operator -- Pow *}
 
 lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
   by (simp add: Pow_def)
@@ -575,7 +575,7 @@
   by (unfold Un_def) blast
 
 
-subsection {* Binary intersection -- Int *}
+subsubsection {* Binary intersection -- Int *}
 
 lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
   by (unfold Int_def) blast
@@ -593,7 +593,7 @@
   by simp
 
 
-subsection {* Set difference *}
+subsubsection {* Set difference *}
 
 lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
   by (unfold set_diff_def) blast
@@ -905,7 +905,7 @@
   done
 
 
-section {* Transitivity rules for calculational reasoning *}
+subsection {* Transitivity rules for calculational reasoning *}
 
 lemma forw_subst: "a = b ==> P b ==> P a"
   by (rule ssubst)