--- a/Quot/Examples/SigmaEx.thy	Sat Jan 23 17:25:18 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Sun Jan 24 23:41:27 2010 +0100
@@ -113,7 +113,8 @@
 translations
   "\<exists>\<exists> x. P"   == "Ex (%x. P)"
 
-lemma split_rsp[quot_respect]: "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
+lemma split_rsp[quot_respect]: 
+  "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split"
 by auto
 
 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
@@ -130,6 +131,8 @@
 lemma operm_rsp[quot_respect]: "(op = ===> alpha_obj ===> alpha_obj) op \<bullet> op \<bullet>"
 sorry
 
+  
+
 lemma liftd: "
 \<exists>\<exists>(hom_o, (hom_d, (hom_e, hom_m))).
 (