# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262765963 -3600
# Node ID e5109811c4d490884bfcde3389420a135f1b8765
# Parent  cd3fa86be45f04efa6c578d93738db041958fafb
Tried to prove the lemma manually; only left with quotient proofs.

diff -r cd3fa86be45f -r e5109811c4d4 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Wed Jan 06 08:24:37 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Wed Jan 06 09:19:23 2010 +0100
@@ -256,11 +256,9 @@
   shows "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx> ===> op \<approx>) concat concat"
 sorry
 
-lemma nil_rsp2: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
-sledgehammer
+lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OO op \<approx> OO list_rel op \<approx>) [] []"
 apply (metis FSet3.nil_rsp list_rel.simps(1) pred_comp.intros)
-atp_minimize [atp=remote_vampire] FSet3.nil_rsp list_rel.simps(1) pred_comp.intros
-thm pred_comp_def
+done
 
 lemma fconcat_empty:
   shows "fconcat {||} = {||}"
@@ -285,9 +283,12 @@
 prefer 2
 apply(rule concat_rsp)
 prefer 3
-thm nil_rsp
-apply(tactic {* rep_abs_rsp_tac @{context} 1 *})
-apply(rule rep_abs_rsp)
+apply(injection)
+prefer 2
+apply(thin_tac "Quot_True {||}")
+apply(unfold Quotient_def)
+
+apply(auto)
 sorry
 
 lemma fconcat_insert: