equal
deleted
inserted
replaced
521 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
521 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
524 done |
524 done |
525 |
525 |
|
526 ML {* #quot_thm (hd (quotdata_dest @{theory})) *} |
|
527 print_quotients |
|
528 thm QUOTIENT_fset |
526 end |
529 end |