diff -r 0dd10a900cae -r 546ba31fbb83 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Wed Dec 09 15:57:47 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 15:59:02 2009 +0100
@@ -373,10 +373,10 @@
 apply (lifting ttt)
 done
 
+
 lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
 sorry
 
-(* PROBLEM *)
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
 apply(lifting ttt2)
 apply(regularize)
@@ -389,6 +389,7 @@
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
 sorry
 
+
 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
@@ -396,9 +397,10 @@
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
-(* PROBLEM *)
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
 apply(lifting hard)
+apply(regularize)
+apply(auto)
 sorry
 
 end