diff -r 98e84b56543f -r d73fa7a3e04b Nominal/FSet.thy
--- a/Nominal/FSet.thy	Fri Oct 15 15:58:48 2010 +0100
+++ b/Nominal/FSet.thy	Fri Oct 15 16:01:03 2010 +0100
@@ -57,9 +57,9 @@
 
 
 definition
-  fminus_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
-  "fminus_raw xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
+  "diff_list xs ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
 
 
 definition
@@ -83,9 +83,9 @@
   shows "set (finter_raw xs ys) = set xs \<inter> set ys"
   by (induct xs) (auto simp add: memb_def)
 
-lemma set_fminus_raw[simp]: 
-  shows "set (fminus_raw xs ys) = (set xs - set ys)"
-  by (auto simp add: fminus_raw_def)
+lemma set_diff_list[simp]: 
+  shows "set (diff_list xs ys) = (set xs - set ys)"
+  by (auto simp add: diff_list_def)
 
 
 section {* Quotient composition lemmas *}
@@ -208,8 +208,8 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
   by simp
 
-lemma fminus_raw_rsp[quot_respect]:
-  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) fminus_raw fminus_raw"
+lemma diff_list_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
   by simp
 
 lemma card_list_rsp[quot_respect]:
@@ -346,7 +346,7 @@
 quotient_definition
   "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
-  "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
 lemma append_finter_raw_distrib:
   "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)"
@@ -720,7 +720,7 @@
 (* FIXME: is this in any case a useful lemma *)
 lemma fin_mdef:
   shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = finsert x (F - {|x|})"
-  by (descending) (auto simp add: memb_def fminus_raw_def)
+  by (descending) (auto simp add: memb_def diff_list_def)
 
 
 subsection {* fset *}
@@ -756,7 +756,7 @@
 
 lemma fminus_set [simp]: 
   shows "fset (xs - ys) = fset xs - fset ys"
-  by (lifting set_fminus_raw)
+  by (lifting set_diff_list)
 
 
 subsection {* funion *}