src/HOL/Library/Product_Plus.thy
changeset 78366 aa4ea5398ab8
parent 64267 b9a1486e79be
equal deleted inserted replaced
78365:bb5e2a7198e3 78366:aa4ea5398ab8