| changeset 26732 | 6ea9de67e576 |
| parent 26513 | 6f306c8c2c54 |
| child 26800 | dcf1dfc915a7 |
--- a/src/HOL/Set.thy Tue Apr 22 08:33:13 2008 +0200 +++ b/src/HOL/Set.thy Tue Apr 22 08:33:16 2008 +0200 @@ -2275,7 +2275,7 @@ begin definition - "eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" + "eq_class.eq A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" instance by default (auto simp add: eq_set_def)