--- 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)