| changeset 499 | f122816d7729 |
| parent 498 | e7bb6bbe7576 |
| child 501 | 375e28eedee7 |
| 498:e7bb6bbe7576 | 499:f122816d7729 |
|---|---|
1233 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1233 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1234 clean_tac lthy quot]] |
1234 clean_tac lthy quot]] |
1235 end) lthy |
1235 end) lthy |
1236 *} |
1236 *} |
1237 |
1237 |
1238 print_quotients |
|
1239 |
|
1240 |
|
1241 end |
1238 end |
1242 |
1239 |