# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260026778 -3600
# Node ID 09cd71fac4eca91d67ea108a81e93bdfe54e8b23
# Parent  d9151fa76f84c111036162e20eb6bb28d8e65c1c
made some slight simplifications to the examples

diff -r d9151fa76f84 -r 09cd71fac4ec IntEx.thy
--- a/IntEx.thy	Sat Dec 05 13:49:35 2009 +0100
+++ b/IntEx.thy	Sat Dec 05 16:26:18 2009 +0100
@@ -153,12 +153,19 @@
 apply(rule refl)
 done
 
+abbreviation 
+  "Abs \<equiv> ABS_my_int"
+abbreviation 
+  "Rep \<equiv> REP_my_int"
+abbreviation 
+  "Resp \<equiv> Respects"
+
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* inj_repabs_tac_intex @{context} 1*})
-(* does not work yet *)
-oops
+apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* clean_tac @{context} 1 *}) 
+done
 
 lemma test2: "my_plus a = my_plus a"
 apply(rule refl)
@@ -166,7 +173,6 @@
 
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
-(* does not work yet *)
 oops
 
 lemma test3: "my_plus = my_plus"
@@ -175,8 +181,6 @@
 
 lemma "PLUS = PLUS"
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
-apply(rule ho_plus_rsp)
-(* does not work yet *)
 oops