# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264504007 -3600
# Node ID 0ff855a6ffb7f4a63fe5c68a340874dfb4512aa4
# Parent  60dd70913b440eaf1fe61fc96f70f413b4cb84bc
Sigma cleaning works with split_prs (still manual proof).

diff -r 60dd70913b44 -r 0ff855a6ffb7 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 11:13:08 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 12:06:47 2010 +0100
@@ -113,12 +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"
-by auto
-
 lemma rvar_rsp[quot_respect]: "(op = ===> alpha_obj) rVar rVar"
-by (simp add: a1)
+  by (simp add: a1)
 
 lemma robj_rsp[quot_respect]: "(list_rel (prod_rel op = alpha_method) ===> alpha_obj) rObj rObj"
 sorry
@@ -150,7 +146,9 @@
 apply (simp)
 prefer 2
 apply cleaning
-apply simp
+apply (subst ex_prs)
+apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
+apply (rule refl)
 sorry
 
 lemma tolift':