diff -r 2d9de77d5687 -r 0dd10a900cae Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -26,20 +26,20 @@
   apply(rule equivp_list_eq)
   done
 
-quotient_def 
-  EMPTY :: "'a fset"
+quotient_def
+  EMPTY :: "EMPTY :: 'a fset"
 where
-  "EMPTY \<equiv> ([]::'a list)"
+  "[]::'a list"
 
-quotient_def 
-  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def
+  INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "INSERT \<equiv> op #"
+  "op #"
 
-quotient_def 
-  FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def
+  FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "FUNION \<equiv> (op @)"
+  "op @"
 
 fun
   membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
@@ -53,10 +53,10 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def 
-  CARD :: "'a fset \<Rightarrow> nat"
+quotient_def
+  CARD :: "CARD :: 'a fset \<Rightarrow> nat"
 where
-  "CARD \<equiv> card1"
+  "card1"
 
 (* text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
@@ -117,19 +117,19 @@
   done
 
 quotient_def
-  IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+  IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
-  "IN \<equiv> membship"
+  "membship"
 
-quotient_def 
-  FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+quotient_def
+  FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "FOLD \<equiv> fold1"
+  "fold1"
 
-quotient_def 
-  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+quotient_def
+  fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> map"
+  "map"
 
 lemma memb_rsp:
   fixes z
@@ -318,14 +318,14 @@
   by (rule equivp_list_eq)
 
 quotient_def
-  EMPTY2 :: "'a fset2"
+  EMPTY2 :: "EMPTY2 :: 'a fset2"
 where
-  "EMPTY2 \<equiv> ([]::'a list)"
+  "[]::'a list"
 
 quotient_def
-  INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+  INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
 where
-  "INSERT2 \<equiv> op #"
+  "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"
 apply (lifting list_induct_part)
@@ -336,14 +336,14 @@
 done
 
 quotient_def
-  fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+  fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "fset_rec \<equiv> list_rec"
+  "list_rec"
 
 quotient_def
-  fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+  fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
-  "fset_case \<equiv> list_case"
+  "list_case"
 
 (* Probably not true without additional assumptions about the function *)
 lemma list_rec_rsp[quot_respect]: