src/HOL/Prod.thy
changeset 1444 23ceb1dc9755
parent 1370 7361ac9b024d
child 1454 d0266c81a85e