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

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

   154 apply(tactic {* regularize_tac @{context} 1 *})

   154 apply(tactic {* regularize_tac @{context} 1 *})

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

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

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

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

   157 done

   157 done

   158 

   160 

   159 lemma test2: "my_plus a = my_plus a"

   161 lemma test2: "my_plus a = my_plus a"

   160 apply(rule refl)

   162 apply(rule refl)

   161 done

   163 done

   162 

   164