# HG changeset patch
# User haftmann
# Date 1325884585 -3600
# Node ID 04a8da7dcffc11373ab81ac46a05c88a8c3b873e
# Parent  2c4d8de91c4ca5b631a97730e7320aecd0bb4b3d
moved lemmas about List.set and set operations to List theory

diff -r 2c4d8de91c4c -r 04a8da7dcffc src/HOL/Quotient_Examples/List_Quotient_Cset.thy
--- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 06 22:16:01 2012 +0100
+++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 06 22:16:25 2012 +0100
@@ -77,7 +77,7 @@
 apply descending
 apply (simp add: Set.remove_def)
 apply descending
-by (simp add: remove_set_compl)
+by (auto simp add: set_eq_iff)
 
 lemma insert_set [code]:
   "Quotient_Cset.insert x (Quotient_Cset.set xs) = Quotient_Cset.set (List.insert x xs)"
@@ -92,7 +92,7 @@
 
 lemma filter_set [code]:
   "Quotient_Cset.filter P (Quotient_Cset.set xs) = Quotient_Cset.set (List.filter P xs)"
-by descending (simp add: project_set)
+by descending (simp add: set_eq_iff)
 
 lemma forall_set [code]:
   "Quotient_Cset.forall (Quotient_Cset.set xs) P \<longleftrightarrow> list_all P xs"