src/HOL/Set.thy
changeset 26513 6f306c8c2c54
parent 26480 544cef16045b
child 26732 6ea9de67e576
     1.1 --- a/src/HOL/Set.thy	Wed Apr 02 15:58:31 2008 +0200
     1.2 +++ b/src/HOL/Set.thy	Wed Apr 02 15:58:32 2008 +0200
     1.3 @@ -2261,13 +2261,6 @@
     1.4    "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)"
     1.5    by simp
     1.6  
     1.7 -instance set :: (eq) eq ..
     1.8 -
     1.9 -lemma eq_set_code [code func]:
    1.10 -  fixes A B :: "'a\<Colon>eq set"
    1.11 -  shows "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.12 -  by auto
    1.13 -
    1.14  lemma subset_eq_code [code func]:
    1.15    fixes A B :: "'a\<Colon>eq set"
    1.16    shows "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    1.17 @@ -2278,6 +2271,16 @@
    1.18    shows "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A"
    1.19    by auto
    1.20  
    1.21 +instantiation set :: (eq) eq
    1.22 +begin
    1.23 +
    1.24 +definition
    1.25 +  "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    1.26 +
    1.27 +instance by default (auto simp add: eq_set_def)
    1.28 +
    1.29 +end
    1.30 +
    1.31  
    1.32  subsubsection {* Derived operations *}
    1.33  
    1.34 @@ -2302,7 +2305,7 @@
    1.35    "Union A = UNION A (\<lambda>x. x)"
    1.36    by auto
    1.37  
    1.38 -code_reserved SML union inter (* Avoid clashes with ML infixes *)
    1.39 +code_reserved SML union inter -- {* avoid clashes with ML infixes *}
    1.40  
    1.41  subsection {* Basic ML bindings *}
    1.42