src/HOL/Library/Product_plus.thy
changeset 56238 5d147e1e18d1
parent 54230 b1d955791529
child 57512 cc97b347b301