# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260307561 -3600
# Node ID 0b29650e3fd8bff03966535924b0a9ec06a9c786
# Parent  830b58c2fa940a4de7915b5c9bd741edc45951a5# Parent  b19c023a3e951e19cc0d3cf46fe1a3ce94ab1c25
merged

diff -r 830b58c2fa94 -r 0b29650e3fd8 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 22:24:24 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 22:26: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