--- a/IntEx.thy	Tue Nov 24 19:09:29 2009 +0100
+++ b/IntEx.thy	Wed Nov 25 03:45:44 2009 +0100
@@ -194,17 +194,6 @@
 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
 done 
 
-apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
-apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
-(* phase 2 *)
-ML_prf {*
- val lower = add_lower_defs @{context} @{thm PLUS_def}
-*}
-apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
-apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
-done
-
-
 
 (*
 does not work.
@@ -236,7 +225,6 @@
 val consts = lookup_quot_consts defs
 *}
 
-ML {* cprem_of *}
 
 ML {* 
 mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)