src/HOL/Library/Product_Vector.thy
changeset 48789 7476665f3e0f
parent 44749 5b1e1432c320
child 49962 a8cc904a6820