| changeset 513 | eed5d55ea9a6 |
| parent 512 | 8c7597b19f0e |
| child 514 | 6b3be083229c |
| 512:8c7597b19f0e | 513:eed5d55ea9a6 |
|---|---|
1285 in |
1285 in |
1286 EVERY1 |
1286 EVERY1 |
1287 [rtac rule, |
1287 [rtac rule, |
1288 RANGE [rtac rthm', |
1288 RANGE [rtac rthm', |
1289 regularize_tac lthy rel_eqv, |
1289 regularize_tac lthy rel_eqv, |
1290 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1290 rtac thm THEN' all_inj_repabs_tac' lthy quot rel_refl trans2, |
1291 clean_tac lthy quot]] |
1291 clean_tac lthy quot]] |
1292 end) lthy |
1292 end) lthy |
1293 *} |
1293 *} |
1294 |
1294 |
1295 end |
1295 end |