diff -r 6decb8811d30 -r 587e97d144a0 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Fri Dec 11 11:12:53 2009 +0100
+++ b/Quot/Examples/FSet.thy	Fri Dec 11 11:14:05 2009 +0100
@@ -27,18 +27,18 @@
   done
 
 quotient_def
-  EMPTY :: "EMPTY :: 'a fset"
-where
+   "EMPTY :: 'a fset"
+as
   "[]::'a list"
 
 quotient_def
-  INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+   "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "op #"
 
 quotient_def
-  FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-where
+   "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+as
   "op @"
 
 fun
@@ -48,8 +48,8 @@
 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
 
 quotient_def
-  CARD :: "CARD :: 'a fset \<Rightarrow> nat"
-where
+   "CARD :: 'a fset \<Rightarrow> nat"
+as
   "card1"
 
 (* text {*
@@ -111,18 +111,18 @@
   done
 
 quotient_def
-  IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
-where
+   "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+as
   "op mem"
 
 quotient_def
-  FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+   "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "fold1"
 
 quotient_def
-  fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
-where
+  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+as
   "map"
 
 lemma mem_rsp:
@@ -275,13 +275,13 @@
   by (rule equivp_list_eq)
 
 quotient_def
-  EMPTY2 :: "EMPTY2 :: 'a fset2"
-where
+   "EMPTY2 :: 'a fset2"
+as
   "[]::'a list"
 
 quotient_def
-  INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
-where
+   "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+as
   "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"
@@ -293,13 +293,13 @@
 done
 
 quotient_def
-  fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+  "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "list_rec"
 
 quotient_def
-  fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
-where
+  "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+as
   "list_case"
 
 (* Probably not true without additional assumptions about the function *)