--- a/Quot/Examples/FSet.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -26,17 +26,17 @@
   fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
    "EMPTY :: 'a fset"
 as
   "[]::'a list"
 
-quotient_def
+quotient_definition
    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "op #"
 
-quotient_def
+quotient_definition
    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 as
   "op @"
@@ -47,7 +47,7 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def
+quotient_definition
    "CARD :: 'a fset \<Rightarrow> nat"
 as
   "card1"
@@ -110,17 +110,17 @@
   apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
   done
 
-quotient_def
+quotient_definition
    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 as
   "op mem"
 
-quotient_def
+quotient_definition
    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "fold1"
 
-quotient_def
+quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 as
   "map"
@@ -274,12 +274,12 @@
 quotient_type fset2 = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def
+quotient_definition
    "EMPTY2 :: 'a fset2"
 as
   "[]::'a list"
 
-quotient_def
+quotient_definition
    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 as
   "op #"
@@ -292,12 +292,12 @@
 apply (lifting list_induct_part)
 done
 
-quotient_def
+quotient_definition
   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_rec"
 
-quotient_def
+quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_case"