equal
deleted
inserted
replaced
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" |
153 apply(rule refl) |
153 apply(rule refl) |
154 done |
154 done |
155 |
|
156 |
|
157 |
155 |
158 lemma "PLUS a = PLUS a" |
156 lemma "PLUS a = PLUS a" |
159 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
157 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) |
160 apply(rule impI) |
158 apply(rule impI) |
161 apply(rule ballI) |
159 apply(rule ballI) |