--- a/IntEx.thy	Sat Dec 05 16:26:18 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 21:28:24 2009 +0100
@@ -173,7 +173,33 @@
 
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
-oops
+apply(rule ballI)
+apply(rule apply_rsp[OF Quotient_my_int ho_plus_rsp])
+apply(simp only: in_respects)
+
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(rule quot_rel_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(fold PLUS_def)
+apply(tactic {* clean_tac @{context} 1 *})
+thm Quotient_rel_rep
+thm Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]]
+apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
+done
 
 lemma test3: "my_plus = my_plus"
 apply(rule refl)
@@ -181,7 +207,18 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
-oops
+apply(rule ho_plus_rsp)
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(rule quot_rel_rsp)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* clean_tac @{context} 1 *})
+apply(simp only: Quotient_rel_rep[OF fun_quotient[OF Quotient_my_int fun_quotient[OF Quotient_my_int Quotient_my_int]]])
+done
 
 
 lemma "PLUS a b = PLUS b a"