diff -r 6decb8811d30 -r 587e97d144a0 Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Fri Dec 11 11:14:05 2009 +0100
@@ -24,23 +24,23 @@
 quotient fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-quotient_def 
-  fempty :: "fempty :: 'a fset" ("{||}")
-where
+quotient_def
+  "fempty :: 'a fset" ("{||}")
+as
   "[]"
 
-quotient_def 
-  finsert :: "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+quotient_def
+  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "(op #)"
 
 lemma finsert_rsp[quot_respect]:
   shows "(op = ===> op \<approx> ===> op \<approx>) (op #) (op #)"
 by (auto intro: list_eq.intros)
 
-quotient_def 
-  funion :: "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
-where
+quotient_def
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+as
   "(op @)"
 
 lemma append_rsp_aux1:
@@ -65,9 +65,9 @@
   by (auto simp add: append_rsp_aux2)
 
 
-quotient_def 
-  fmem :: " fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-where
+quotient_def
+  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+as
   "(op mem)"
 
 lemma memb_rsp_aux:
@@ -89,9 +89,9 @@
 where
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
-quotient_def 
-  finter :: "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
-where
+quotient_def
+  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+as
   "inter_list"
 
 no_syntax