src/HOL/Library/Product_plus.thy
changeset 35536 1f980bbc6ad8
parent 30018 690c65b8ad1a
child 36627 39b2516a1970