# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261866046 -3600
# Node ID 64f9c76f70c7ec3f7d97ef7a80cf0737744ccb6a
# Parent  a28f805df355f7dea48f2a468bfebc4306feccf0
corrected wrong [quot_respect] attribute; tuned

diff -r a28f805df355 -r 64f9c76f70c7 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -93,8 +93,8 @@
 
 ML {*
 test_funs absF @{context} 
-     (@{typ "('a list) list \<Rightarrow> 'a"}, 
-      @{typ "('a fset) fset \<Rightarrow> 'a"})
+     (@{typ "('a list) list \<Rightarrow> 'a list"}, 
+      @{typ "('a fset) fset \<Rightarrow> 'a fset"})
 *}
 
 
diff -r a28f805df355 -r 64f9c76f70c7 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -600,5 +600,7 @@
 apply (lifting list.cases(2))
 done
 
+thm quot_respect
+
 
 end
diff -r a28f805df355 -r 64f9c76f70c7 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/QuotList.thy	Sat Dec 26 23:20:46 2009 +0100
@@ -125,7 +125,7 @@
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-lemma foldr_prs[quot_respect]:
+lemma foldr_prs[quot_preserve]:
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
diff -r a28f805df355 -r 64f9c76f70c7 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Dec 26 21:36:20 2009 +0100
+++ b/Quot/quotient_term.ML	Sat Dec 26 23:20:46 2009 +0100
@@ -228,7 +228,7 @@
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 
-(* FIXME: check that the types correspond to each other? *)
+(* FIXME: check that the types correspond to each other *)
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty