diff -r df053507edba -r 37285ec4387d Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -24,12 +24,12 @@
 quotient_type fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
   "fempty :: 'a fset" ("{||}")
 as
   "[]"
 
-quotient_def
+quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "(op #)"
@@ -38,7 +38,7 @@
   shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
 by (auto intro: list_eq.intros)
 
-quotient_def
+quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
 as
   "(op @)"
@@ -65,7 +65,7 @@
   by (auto simp add: append_rsp_aux2)
 
 
-quotient_def
+quotient_definition
   "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
 as
   "(op mem)"
@@ -89,7 +89,7 @@
 where
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
-quotient_def
+quotient_definition
   "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
 as
   "inter_list"