diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Examples/FSet.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -28,17 +28,17 @@
 
 quotient_definition
    "EMPTY :: 'a fset"
-as
+is
   "[]::'a list"
 
 quotient_definition
    "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "op #"
 
 quotient_definition
    "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-as
+is
   "op @"
 
 fun
@@ -49,12 +49,12 @@
 
 quotient_definition
    "CARD :: 'a fset \<Rightarrow> nat"
-as
+is
   "card1"
 
 quotient_definition
   "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
-as
+is
   "concat"
 
 term concat
@@ -120,17 +120,17 @@
 
 quotient_definition
    "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-as
+is
   "op mem"
 
 quotient_definition
    "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "fold1"
 
 quotient_definition
   "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-as
+is
   "map"
 
 lemma mem_rsp:
@@ -285,12 +285,12 @@
 
 quotient_definition
    "EMPTY2 :: 'a fset2"
-as
+is
   "[]::'a list"
 
 quotient_definition
    "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-as
+is
   "op #"
 
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
@@ -303,12 +303,12 @@
 
 quotient_definition
   "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_rec"
 
 quotient_definition
   "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-as
+is
   "list_case"
 
 (* Probably not true without additional assumptions about the function *)