--- a/IntEx.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -1,7 +1,6 @@
 theory IntEx
 imports QuotMain
 begin
-  
 
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
@@ -237,12 +236,12 @@
 by (simp_all add: Quotient_ABS_REP[OF a])
 
 lemma cons_rsp[quotient_rsp]:
-  "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
+  "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #"
 by simp
 
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
-  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
+  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
 apply (simp only: fun_rel.simps)
 apply (rule allI)
 apply (rule allI)
@@ -257,7 +256,7 @@
 sorry
 
 lemma nil_listrel_rsp[quotient_rsp]:
-  "(LIST_REL R) [] []"
+  "(list_rel R) [] []"
 by simp
 
 lemma "foldl PLUS x [] = x"