# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259931503 -3600
# Node ID c7c6ba5ac043c8ce32818dbae5d2819a91df8278
# Parent  1a4eb39ba83495d73f1c273d580fd989e614e635
some tuning

diff -r 1a4eb39ba834 -r c7c6ba5ac043 FSet.thy
--- a/FSet.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/FSet.thy	Fri Dec 04 13:58:23 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 1a4eb39ba834 -r c7c6ba5ac043 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 13:58:23 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} "*" *}