src/HOL/Prod.thy
changeset 2434 d3d42a2e7da2
parent 2393 651fce76c86c
child 2880 a0fde30aa126