--- a/IntEx.thy	Tue Oct 27 07:46:52 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 09:01:12 2009 +0100
@@ -110,10 +110,6 @@
 where
  "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))"
 
-lemma plus_sym_pre:
-  shows "intrel (my_plus a b) (my_plus b a)"
-  sorry
-
 lemma equiv_intrel: "EQUIV intrel"
   sorry
 
@@ -135,9 +131,40 @@
 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *}
 ML {* val t_defs = @{thms PLUS_def} *}
 
+ML {*
+fun lift_thm_my_int lthy t =
+  lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t
+*}
+
+lemma plus_sym_pre:
+  shows "intrel (my_plus a b) (my_plus b a)"
+  apply (cases a)
+  apply (cases b)
+  apply (simp)
+  done
+
+ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *}
+
+lemma plus_assoc_pre:
+  shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))"
+  apply (cases i)
+  apply (cases j)
+  apply (cases k)
+  apply (simp add: intrel_refl)
+  done
+
+ ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
 
 
-ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
+
+
+
+
+
+
+text {* Below is the construction site code used if things do now work *}
+
+ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
 ML {* val (g, thm, othm) =
@@ -173,11 +200,5 @@
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
 
-lemma 
-  fixes i j k::"my_int"
-  shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))"
-  apply(unfold PLUS_def)
-  apply(simp add: expand_fun_eq)
-  sorry