src/HOL/Library/Quotient_Sum.thy
changeset 52861 e93d73b51fd0
parent 51994 82cc2aeb7d13
child 53010 ec5e6f69bd65