src/HOL/Quotient_Examples/Lift_Fun.thy

--- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Fri Mar 23 14:17:29 2012 +0100
@@ -23,17 +23,17 @@
   by (simp add: identity_equivp)
 
 quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"  is
-  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+  "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done
 
 quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is 
-  fcomp
+  fcomp done
 
 quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd" 
-  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
+  is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done
 
-quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on
+quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done
 
-quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw
+quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done
 
 
 subsection {* Co/Contravariant type variables *} 
@@ -47,7 +47,7 @@
   where "map_endofun' f g e = map_fun g f e"
 
 quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
-  map_endofun'
+  map_endofun' done
 
 text {* Registration of the map function for 'a endofun. *}
 
@@ -63,7 +63,7 @@
     by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc) 
 qed
 
-quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
+quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
 
 term  endofun_id_id
 thm  endofun_id_id_def
@@ -73,7 +73,7 @@
 text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting)
   over a type variable which is a covariant and contravariant type variable. *}
 
-quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id
+quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done
 
 term  endofun'_id_id
 thm  endofun'_id_id_def