# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260287811 -3600
# Node ID 793c3ff4bc2ab25d6d6834d6d83c117023ee30bd
# Parent  54573efed52767c89228602bc1d27d207a03152a# Parent  2e51e13158391de70d0fdd0be5a811da1a90a3d5
merge

diff -r 2e51e1315839 -r 793c3ff4bc2a Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 16:56:51 2009 +0100
@@ -434,11 +434,14 @@
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-defer
+apply(rule impI)
+apply(simp)
+apply(rule allI)
+apply(rule list_eq_refl)
 apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
-sorry
+done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
 sorry