diff -r 68c1f378a70a -r 0879d144aaa3 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 09:28:32 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 09:54:43 2010 +0100
@@ -377,22 +377,6 @@
 apply(assumption)
 done
 
-lemma [quot_respect]:
-  "((op \<approx> ===> op \<approx> ===> op =) ===> prod_rel op \<approx> op \<approx> ===> op =) split split"
-apply(simp)
-done
-
-thm quot_preserve
-term split
-
-
-lemma [quot_preserve]:
-  shows "(((abs_fset ---> abs_fset ---> id) ---> prod_fun rep_fset rep_fset ---> id) split) = split"
-apply(simp add: expand_fun_eq)
-apply(simp add: Quotient_abs_rep[OF Quotient_fset])
-done
-
-
 lemma test: "All (\<lambda>(x::'a list, y). x = y)"
 sorry