--- a/FSet.thy	Tue Dec 01 14:08:56 2009 +0100
+++ b/FSet.thy	Tue Dec 01 16:27:42 2009 +0100
@@ -12,6 +12,12 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
+lemma
+  "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)"
+apply(simp add: FUN_REL.simps)
+apply(rule allI | rule impI)+
+sorry
+
 lemma list_eq_refl:
   shows "xs \<approx> xs"
   by (induct xs) (auto intro: list_eq.intros)

--- a/QuotMain.thy	Tue Dec 01 14:08:56 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 16:27:42 2009 +0100
@@ -836,12 +836,24 @@
 
 *)
 
+definition 
+  "QUOT_TRUE x \<equiv> True"
+
+lemma quot_true_dests:
+  shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
+  and   QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A"
+  and   QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B"
+  and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
+apply(simp_all add: QUOT_TRUE_def)
+done
+
+
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2),
+    DT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     NDT ctxt "2" (lambda_res_tac ctxt),
@@ -887,12 +899,6 @@
     (* resolving with R x y assumptions *)
     NDT ctxt "E" (atac),
 
-    (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
-    
-    (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)
-
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
     NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
@@ -929,7 +935,7 @@
       if incr_boundvars i u aconv t then Bound i
       else (case t of
         t1 $ t2 => mk_abs i t1 $ mk_abs i t2
-      | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
+      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
       | Bound j => if i = j then error "make_inst" else t
       | _ => t);
   in (f, Abs ("x", T, mk_abs 0 g)) end;
@@ -986,21 +992,30 @@
  The first two need to be done before fun_map is unfolded
 
  - LAMBDA_PRS:
-     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))       \<Longrightarrow>   f
+     (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
+
  - FORALL_PRS (and the same for exists: EXISTS_PRS)
-     \<forall>x\<in>Respects R. (abs ---> id) ?f                \<Longrightarrow>   \<forall>x. ?f
+     \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
+
  - Rewriting with definitions from the argument defs
-     NewConst                                       \<Longrightarrow>   (rep ---> abs) oldConst
+     NewConst  ---->  (rep ---> abs) oldConst
+
  - QUOTIENT_REL_REP:
-     Rel (Rep x) (Rep y)                            \<Longrightarrow>   x = y
+     Rel (Rep x) (Rep y)  ---->  x = y
+
  - ABS_REP
-     Abs (Rep x)                                    \<Longrightarrow>   x
+     Abs (Rep x)  ---->  x
+
  - id_simps; fun_map.simps
 
  The first one is implemented as a conversion (fast).
  The second one is an EqSubst (slow).
  The rest are a simp_tac and are fast.
 *)
+
+thm all_prs ex_prs
+
+
 ML {*
 fun clean_tac lthy quot defs =
   let