src/HOL/Library/Product_plus.thy
changeset 54110 1d6d2ce2ad3e
parent 51301 6822aa82aafa
child 54230 b1d955791529