src/HOL/Library/Quotient_Sum.thy
changeset 47863 ec5d54029664
parent 47777 f29e7dcd7c40
child 47936 756f30eac792