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.11    by (simp add: Pow_def)
    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)