# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260306301 -3600
# Node ID b19c023a3e951e19cc0d3cf46fe1a3ce94ab1c25
# Parent  10d04ee5210184be07a5567d3d627e2fdf1c7fca# Parent  fe2a37cfecd3c9e287cc6dfd2ec255d9d33b8182
merge

diff -r fe2a37cfecd3 -r b19c023a3e95 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:02:14 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 22:05:01 2009 +0100
@@ -444,4 +444,22 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
+lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
+sorry
+
+lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
+apply(lifting_setup hard)
+defer
+apply(injection)
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(subst babs_prs)
+defer defer
+apply(tactic {* lambda_prs_tac @{context} 1 *})
+(* Until here is ok *)
+apply(cleaning)
 end