--- a/FSet.thy	Tue Dec 01 18:51:14 2009 +0100
+++ b/FSet.thy	Tue Dec 01 19:01:51 2009 +0100
@@ -291,24 +291,6 @@
   apply (auto simp add: memb_rsp rsp_fold_def)
 done
 
-lemma list_eq_rsp[quot_rsp]:
-  "(op \<approx> ===> op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
-apply(simp add: FUN_REL.simps)
-apply(auto)
-apply(blast intro: list_eq.intros)
-apply(blast intro: list_eq.intros)
-done
-
-lemma list_eq_rsp2[quot_rsp]:
-  "(op \<approx> ===> op =) (op \<approx>) (op \<approx>)"
-apply(simp add: FUN_REL.simps)
-apply(rule allI)+
-apply(rule impI)
-apply(simp add: expand_fun_eq)
-apply(rule allI)
-apply(blast intro: list_eq.intros)
-done
-
 print_quotients
 
 ML {* val qty = @{typ "'a fset"} *}
@@ -357,51 +339,6 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-apply(tactic {* procedure_tac @{context} @{thm map_append} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})
- 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})
-back 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) 
-
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
 
@@ -420,14 +357,22 @@
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i)
 
-apply (drule QT_all)
-apply (drule_tac x = "x" in QT_lam)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply (drule QT_all)
-apply (drule_tac x = "y" in QT_lam)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* lambda_res_tac @{context} 1 *})
+apply(tactic {* rule FUN_REL_I)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(clarify)
+apply (drule_tac x="x" in QT_lam)
+
+
+
+thm QT_lam
+apply (drule QT_all)
+apply (drule_tac x = "yyy" in QT_lam)
 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 

--- a/QuotMain.thy	Tue Dec 01 18:51:14 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 19:01:51 2009 +0100
@@ -905,7 +905,7 @@
 
 ML {*
 fun quot_true_tac ctxt fnctn =
-  SUBGOAL (fn (gl, _) =>
+  SUBGOAL (fn (gl, i) =>
   let
     val thy = ProofContext.theory_of ctxt;
     fun find_fun trm =
@@ -923,7 +923,7 @@
           val cty2 = ctyp_of thy (fastype_of fx);
           val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
         in
-          dtac thm 1
+          dtac thm i
         end
     | NONE => error "quot_true_tac!"
     | _ => error "quot_true_tac!!"