# HG changeset patch
# User haftmann
# Date 1254323061 -7200
# Node ID 371c7f74282d7ddd71c5a3a5bcfc7a04592935ab
# Parent  8ae3a48c69d9f8295e2be04c11fd1fbf05a6d2d5
tuned headings

diff -r 8ae3a48c69d9 -r 371c7f74282d src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 30 11:45:42 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 30 17:04:21 2009 +0200
@@ -34,7 +34,7 @@
   by (auto simp add: sup_bool_eq)
 
 
-subsubsection {* Equality and Subsets *}
+subsubsection {* Equality *}
 
 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
   by (simp add: mem_def)
@@ -42,6 +42,9 @@
 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
   by (simp add: expand_fun_eq mem_def)
 
+
+subsubsection {* Order relation *}
+
 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
   by (simp add: mem_def)
 
@@ -63,9 +66,6 @@
 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
   by (simp add: bot_fun_eq bot_bool_eq)
 
-
-subsubsection {* The empty set *}
-
 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   by (auto simp add: expand_fun_eq)