diff -r 2e51e1315839 -r 520a4084d064 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -177,7 +177,7 @@
   shows "(z memb x) = (z memb y)"
   using a by induct auto
 
-lemma ho_memb_rsp[quotient_rsp]:
+lemma ho_memb_rsp[quot_respect]:
   "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
   by (simp add: memb_rsp)
 
@@ -187,17 +187,17 @@
   shows "card1 a = card1 b"
   using e by induct (simp_all add:memb_rsp)
 
-lemma ho_card1_rsp[quotient_rsp]: 
+lemma ho_card1_rsp[quot_respect]: 
   "(op \<approx> ===> op =) card1 card1"
   by (simp add: card1_rsp)
 
-lemma cons_rsp[quotient_rsp]:
+lemma cons_rsp[quot_respect]:
   fixes z
   assumes a: "xs \<approx> ys"
   shows "(z # xs) \<approx> (z # ys)"
   using a by (rule list_eq.intros(5))
 
-lemma ho_cons_rsp[quotient_rsp]:
+lemma ho_cons_rsp[quot_respect]:
   "(op = ===> op \<approx> ===> op \<approx>) op # op #"
   by (simp add: cons_rsp)
 
@@ -254,7 +254,7 @@
   apply (rule append_sym_rsp)
   done
 
-lemma ho_append_rsp[quotient_rsp]:
+lemma ho_append_rsp[quot_respect]:
   "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (simp add: append_rsp)
 
@@ -266,7 +266,7 @@
   apply(auto intro: list_eq.intros)
   done
 
-lemma ho_map_rsp[quotient_rsp]:
+lemma ho_map_rsp[quot_respect]:
   "(op = ===> op \<approx> ===> op \<approx>) map map"
   by (simp add: map_rsp)
 
@@ -274,7 +274,7 @@
   "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
  by simp (rule list_eq_refl)
 
-lemma ho_fold_rsp[quotient_rsp]:
+lemma ho_fold_rsp[quot_respect]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
   apply (auto)
   apply (case_tac "rsp_fold x")
@@ -286,7 +286,7 @@
   apply (auto simp add: memb_rsp rsp_fold_def)
 done
 
-lemma list_equiv_rsp[quotient_rsp]:
+lemma list_equiv_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
 by (auto intro: list_eq.intros)
 
@@ -355,8 +355,6 @@
   apply (assumption)
   done
 
-thm quotient_thm
-
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* lift_tac @{context} @{thm list_induct_part} 1 *})
 done
@@ -402,14 +400,14 @@
   "fset_case \<equiv> list_case"
 
 (* Probably not true without additional assumptions about the function *)
-lemma list_rec_rsp[quotient_rsp]:
+lemma list_rec_rsp[quot_respect]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
   apply (auto)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
-lemma list_case_rsp[quotient_rsp]:
+lemma list_case_rsp[quot_respect]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
   apply (auto)
   sorry