src/HOL/Library/Quotient_Sum.thy
changeset 54381 9c1f21365326
parent 53026 e1a548c11845
child 55564 e81ee43ab290