# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255774856 -7200
# Node ID b441019d457db72a4435dd8999911a43d1eea5f0
# Parent  13575d73e435b99bc19cf1e5e9d33286908c0980
Further in the proof

diff -r 13575d73e435 -r b441019d457d QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 11:54:50 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:20:56 2009 +0200
@@ -1317,9 +1317,26 @@
 ML_prf {* man_inst_norm *}
 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *})
 
-
+(* MINE *)
+apply (rule QUOTIENT_fset)
 
-
+prefer 3
+(* ABS_REP_RSP *)
+thm REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]
+apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"])
+(* MINE *)
+apply (rule QUOTIENT_fset)
+(* MINE *)
+apply (rule list_eq_refl )
+prefer 2
+(* ABS_REP_RSP *)
+apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"])
+prefer 2
+(* MINE *)
+apply (simp only: FUN_REL.simps)
+prefer 3
+(* APPLY_RSP *)
+thm APPLY_RSP
 sorry
 
 thm list.recs(2)