src/HOL/Library/Quotient_Sum.thy
changeset 49088 5cd8b4426a57
parent 47982 7aa35601ff65
child 51377 7da251a6c16e