# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259932280 -3600
# Node ID 7ba2fc25c6a3af6ac8fffe833e4a52fa0b76c8d0
# Parent  3f657c4fbefa27e63c2574af502c4b83f0fd22a6# Parent  c7c6ba5ac043c8ce32818dbae5d2819a91df8278
merge

diff -r 3f657c4fbefa -r 7ba2fc25c6a3 FSet.thy
--- a/FSet.thy	Fri Dec 04 14:11:03 2009 +0100
+++ b/FSet.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -337,8 +337,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-lemma cheat: "P" sorry
-
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
diff -r 3f657c4fbefa -r 7ba2fc25c6a3 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 14:11:03 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 14:11:20 2009 +0100
@@ -146,7 +146,7 @@
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
 lemmas [quotient_thm] = 
-  FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+  FUN_QUOTIENT LIST_QUOTIENT
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}