# HG changeset patch
# User nipkow
# Date 1362738500 -3600
# Node ID 65f4284d3f1a57d1a14cc29214025c4166c5592b
# Parent  197ad6b8f7630b80662245a1b2cc0158270707d5# Parent  d315e9a9ee72ab549a46dae48be51b056983346c
merged

diff -r d315e9a9ee72 -r 65f4284d3f1a src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Fri Mar 08 11:28:04 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Fri Mar 08 11:28:20 2013 +0100
@@ -470,6 +470,8 @@
   unfolding fset_rel_def fset_rel_aux by simp
 qed auto
 
+lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
+
 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
 unfolding fset_rel_def set_rel_def by auto 
 
diff -r d315e9a9ee72 -r 65f4284d3f1a src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 08 11:28:04 2013 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Mar 08 11:28:20 2013 +0100
@@ -722,6 +722,9 @@
   shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
   by (descending) (simp)
 
+lemma in_fset_map_fset[simp]: "a |\<in>| map_fset f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
+  by descending auto
+
 
 subsection {* card_fset *}