src/HOL/Set.thy
 changeset 12023 d982f98e0f0d parent 12020 a24373086908 child 12114 a8e860c86252
```     1.1 --- a/src/HOL/Set.thy	Sat Nov 03 01:33:33 2001 +0100
1.2 +++ b/src/HOL/Set.thy	Sat Nov 03 01:33:54 2001 +0100
1.3 @@ -515,7 +515,7 @@
1.4    by (blast elim: equalityE)
1.5
1.6
1.7 -section {* The Powerset operator -- Pow *}
1.8 +subsubsection {* The Powerset operator -- Pow *}
1.9
1.10  lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
1.12 @@ -575,7 +575,7 @@
1.13    by (unfold Un_def) blast
1.14
1.15
1.16 -subsection {* Binary intersection -- Int *}
1.17 +subsubsection {* Binary intersection -- Int *}
1.18
1.19  lemma Int_iff [simp]: "(c : A Int B) = (c:A & c:B)"
1.20    by (unfold Int_def) blast
1.21 @@ -593,7 +593,7 @@
1.22    by simp
1.23
1.24
1.25 -subsection {* Set difference *}
1.26 +subsubsection {* Set difference *}
1.27
1.28  lemma Diff_iff [simp]: "(c : A - B) = (c:A & c~:B)"
1.29    by (unfold set_diff_def) blast
1.30 @@ -905,7 +905,7 @@
1.31    done
1.32
1.33
1.34 -section {* Transitivity rules for calculational reasoning *}
1.35 +subsection {* Transitivity rules for calculational reasoning *}
1.36
1.37  lemma forw_subst: "a = b ==> P b ==> P a"
1.38    by (rule ssubst)
```