diff -r 5be8e34c2c0e -r 6bf332360510 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Sun Nov 14 10:02:30 2010 +0000
+++ b/Nominal/Nominal2_FSet.thy	Sun Nov 14 11:05:22 2010 +0000
@@ -1,75 +1,8 @@
 theory Nominal2_FSet
 imports "../Nominal-General/Nominal2_Base"
-        "../Nominal-General/Nominal2_Eqvt" 
-        "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet"
-begin
-
-lemma permute_fset_rsp[quot_respect]:
-  shows "(op = ===> list_eq ===> list_eq) permute permute"
-  unfolding fun_rel_def
-  by (simp add: set_eqvt[symmetric])
-
-instantiation fset :: (pt) pt
+        "../Nominal-General/Nominal2_Eqvt"
 begin
 
-quotient_definition
-  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
-  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-instance 
-proof
-  fix x :: "'a fset" and p q :: "perm"
-  show "0 \<bullet> x = x" by (descending) (simp)
-  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
-qed
-
-end
-
-lemma permute_fset[simp, eqvt]:
-  fixes S::"('a::pt) fset"
-  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
-  and   "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
-  by (lifting permute_list.simps)
-
-lemma map_fset_eqvt[eqvt]: 
-  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
-  by (lifting map_eqvt)
-
-lemma fset_eqvt[eqvt]: 
-  shows "p \<bullet> (fset S) = fset (p \<bullet> S)"
-  by (lifting set_eqvt)
-
-lemma supp_fset [simp]:
-  shows "supp (fset S) = supp S"
-  unfolding supp_def
-  by (perm_simp) (simp add: fset_cong)
-
-lemma supp_empty_fset [simp]:
-  shows "supp {||} = {}"
-  unfolding supp_def
-  by simp
-
-lemma supp_insert_fset [simp]:
-  fixes x::"'a::fs"
-  and   S::"'a fset"
-  shows "supp (insert_fset x S) = supp x \<union> supp S"
-  apply(subst supp_fset[symmetric])
-  apply(simp add: supp_fset supp_of_fin_insert)
-  done
-
-lemma fset_finite_supp:
-  fixes S::"('a::fs) fset"
-  shows "finite (supp S)"
-  by (induct S) (simp_all add: finite_supp)
-
-
-subsection {* finite sets are fs-types *}
-
-instance fset :: (fs) fs
-  apply (default)
-  apply (rule fset_finite_supp)
-  done
 
 lemma atom_map_fset_cong:
   shows "map_fset atom x = map_fset atom y \<longleftrightarrow> x = y"
@@ -100,7 +33,7 @@
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
-  apply (simp add: supp_of_fin_insert)
+  apply (simp add: supp_of_finite_insert)
   apply (rule conjI)
   apply (unfold fresh_star_def)
   apply simp