src/HOL/Library/Quotient_Sum.thy
changeset 47372 9ab4e22dac7b
parent 47308 9caab698dbe4
child 47455 26315a545e26