--- a/FSet.thy	Tue Nov 24 19:09:29 2009 +0100
+++ b/FSet.thy	Wed Nov 25 03:45:44 2009 +0100
@@ -376,6 +376,7 @@
           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
 *}
 
+(*
 ML {*
 lambda_prs_conv @{context} quot 
 @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x\<Colon>'a list \<Rightarrow> bool. id ((f ((REP_fset ---> id) x) ((REP_fset ---> id) x))))"}
@@ -395,15 +396,16 @@
                         (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list)))))"}
 
 *}
-
+*)
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+oops
 
-
+(*
 thm LAMBDA_PRS
 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *})
 
@@ -414,19 +416,17 @@
 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
-ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
-
-
+ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}*)
 
 
-thm map_append
-lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+lemma "\<forall>f x xa. fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
-apply(tactic {* prepare_tac 1 *})
-thm map_append
-apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
-done
+oops
+
 
+lemma "fmap f (FUNION (x::'b fset) (y::'b fset)) = FUNION (fmap f x) (fmap f y)"
+apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
+oops
 
 
 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"