src/HOL/Library/Product_Vector.thy
changeset 30077 c5920259850c
parent 30019 a2f19e0a28b2
child 30729 461ee3e49ad3