# HG changeset patch
# User haftmann
# Date 1164708136 -3600
# Node ID 7442833ea2b6bf075cd584cfc29212b1232a4973
# Parent  6096c956a11fb6ab2f64ac47eb62926966648e20
added strict_subset

diff -r 6096c956a11f -r 7442833ea2b6 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Tue Nov 28 00:35:28 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Nov 28 11:02:16 2006 +0100
@@ -27,14 +27,28 @@
 
 lemmas [symmetric, code inline] = subset_def
 
+definition
+  strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where 
+  "strict_subset = op \<subset>"
+
+lemmas [symmetric, code inline] = strict_subset_def
+
 lemma [code target: Set]:
   "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   by blast
 
 lemma [code func]:
+  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+  by blast
+
+lemma [code func]:
   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   unfolding subset_def Set.subset_def ..
 
+lemma [code func]:
+  "strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B"
+  unfolding subset_def strict_subset_def by blast
+
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..