src/HOL/Analysis/Product_Vector.thy
changeset 67505 ceb324e34c14
parent 66453 cc19f7ca2ed6
child 67685 bdff8bf0a75b
equal deleted inserted replaced
67504:310114bec0d7 67505:ceb324e34c14