equal
deleted
inserted
replaced
139 lemma test1: "my_plus a b = my_plus a b" |
139 lemma test1: "my_plus a b = my_plus a b" |
140 apply(rule refl) |
140 apply(rule refl) |
141 done |
141 done |
142 |
142 |
143 lemma "PLUS a b = PLUS a b" |
143 lemma "PLUS a b = PLUS a b" |
144 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) |
144 apply(lifting_setup rule: test1) |
145 apply(tactic {* regularize_tac @{context} 1 *}) |
145 apply(regularize) |
146 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
146 apply(injection) |
147 apply(tactic {* clean_tac @{context} 1 *}) |
147 apply(cleaning) |
148 done |
148 done |
149 |
149 |
150 thm lambda_prs |
150 thm lambda_prs |
151 |
151 |
152 lemma test2: "my_plus a = my_plus a" |
152 lemma test2: "my_plus a = my_plus a" |