src/HOL/Library/Product_plus.thy
changeset 63285 e9c777bfd78c
parent 60679 ade12ef2773c