--- a/IntEx.thy	Wed Nov 25 10:34:03 2009 +0100
+++ b/IntEx.thy	Wed Nov 25 10:39:53 2009 +0100
@@ -136,28 +136,21 @@
 ML {* val ty_name = "my_int" *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val defs = @{thms PLUS_def} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
+ML {* val consts = lookup_quot_consts defs *}
 
 ML {*
 fun lift_thm_my_int lthy t =
   lift_thm lthy qty ty_name rsp_thms defs t
-*}
-
-ML {*
 fun lift_thm_g_my_int lthy t g =
   lift_thm_goal lthy qty ty_name rsp_thms defs t g
+fun lift_tac_fset lthy t =
+  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs
 *}
 
-print_quotients
-ML {* quotdata_lookup @{context} "IntEx.my_int" *}
-ML {* quotdata_lookup @{context} "my_int" *}
-
-ML {*
-  val test = lift_thm_my_int @{context} @{thm plus_sym_pre}
-*}
-
-ML {*
-  lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "PLUS a b = PLUS b a"}
-*}
+lemma "PLUS a b = PLUS b a"
+by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *})
 
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -167,10 +160,9 @@
   apply (simp)
   done
 
-ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
+lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
+by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *})
 
-ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} 
-         @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *}
 
 ML {*
   mk_REGULARIZE_goal @{context} 
@@ -286,27 +278,7 @@
 *}
 
 
-lemma foldl_rsp:
-  "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>
-           IntEx.intrel ===> op = ===> IntEx.intrel)
-           foldl foldl"
-  apply (simp only:FUN_REL.simps)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  apply (rule allI)
-  apply (rule allI)
-  apply (rule impI)
-  apply (simp only:)
-  apply (rule list.induct)
-  apply (simp)
-  apply (simp only: foldl.simps)
-  sorry
 
-ML {* val rsp_thms = @{thm foldl_rsp} :: rsp_thms *}
 prove t_t: rg
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}