diff -r df053507edba -r 37285ec4387d Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sun Dec 20 00:26:53 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sun Dec 20 00:53:35 2009 +0100
@@ -209,15 +209,15 @@
 
 section {* Constants on the Quotient Type *} 
 
-quotient_def
+quotient_definition
   "fempty :: 'a fset" 
   as "[]::'a list"
 
-quotient_def
+quotient_definition
   "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
   as "op #"
 
-quotient_def
+quotient_definition
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
   as "\<lambda>x X. x \<in> set X"
 
@@ -226,27 +226,27 @@
 where
   "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
 
-quotient_def
+quotient_definition
   "fcard :: 'a fset \<Rightarrow> nat" 
   as "card_raw"
 
-quotient_def
+quotient_definition
   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
   as "delete_raw"
 
-quotient_def
+quotient_definition
   "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
   as "op @"
 
-quotient_def
+quotient_definition
   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
   as "inter_raw"
 
-quotient_def
+quotient_definition
   "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" 
   as "fold_raw"
 
-quotient_def
+quotient_definition
   "fset_to_set :: 'a fset \<Rightarrow> 'a set" 
   as "set"
 
@@ -304,7 +304,7 @@
 lemma "funion (funion x xa) xb = funion x (funion xa xb)"
 by (lifting append_assoc)
 
-quotient_def
+quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 as
   "list_case"