src/HOL/Library/Quotient_Sum.thy
changeset 51796 f0ee854aa2bd
parent 51377 7da251a6c16e
child 51956 a4d81cdebf8b