| changeset 603 | 7f35355df72e |
| parent 602 | e56eeb9fedb3 |
| parent 601 | 81f40b8bde7b |
| child 605 | 120e479ed367 |
| 602:e56eeb9fedb3 | 603:7f35355df72e |
|---|---|
270 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
270 apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) |
271 defer |
271 defer |
272 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
272 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) |
273 apply(tactic {* clean_tac @{context} 1 *}) |
273 apply(tactic {* clean_tac @{context} 1 *}) |
274 sorry |
274 sorry |
275 |
|
276 end |