| changeset 601 | 81f40b8bde7b |
| parent 600 | 5d932e7a856c |
| child 603 | 7f35355df72e |
| 600:5d932e7a856c | 601:81f40b8bde7b |
|---|---|
272 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
272 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
273 defer |
273 defer |
274 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
274 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
275 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
275 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
276 sorry |
276 sorry |
277 |
|
278 end |