152 abbreviation 

   152 abbreviation 

   153   "Rep \<equiv> REP_my_int"

   153   "Rep \<equiv> REP_my_int"

   154 abbreviation 

   154 abbreviation 

   155   "Resp \<equiv> Respects"

   155   "Resp \<equiv> Respects"

   156 

   156 

   157 lemma "PLUS a b = PLUS a b"

   158 lemma "PLUS a b = PLUS a b"

   158 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})

   159 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})

   159 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})

   160 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})

   160 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   161 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})

   161 apply(tactic {* clean_tac @{context} 1 *}) 

   163 apply(tactic {* clean_tac @{context} 1 *}) 

   162 done

   164 done

   163 

   165 

   164 lemma test2: "my_plus a = my_plus a"

   166 lemma test2: "my_plus a = my_plus a"

   165 apply(rule refl)

   167 apply(rule refl)