src/HOL/Predicate.thy
changeset 32779 371c7f74282d
parent 32705 04ce6bb14d85
child 32782 faf347097852
     1.1 --- a/src/HOL/Predicate.thy	Wed Sep 30 11:45:42 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Sep 30 17:04:21 2009 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    by (auto simp add: sup_bool_eq)
     1.5  
     1.6  
     1.7 -subsubsection {* Equality and Subsets *}
     1.8 +subsubsection {* Equality *}
     1.9  
    1.10  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
    1.11    by (simp add: mem_def)
    1.12 @@ -42,6 +42,9 @@
    1.13  lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
    1.14    by (simp add: expand_fun_eq mem_def)
    1.15  
    1.16 +
    1.17 +subsubsection {* Order relation *}
    1.18 +
    1.19  lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
    1.20    by (simp add: mem_def)
    1.21  
    1.22 @@ -63,9 +66,6 @@
    1.23  lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
    1.24    by (simp add: bot_fun_eq bot_bool_eq)
    1.25  
    1.26 -
    1.27 -subsubsection {* The empty set *}
    1.28 -
    1.29  lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
    1.30    by (auto simp add: expand_fun_eq)
    1.31