src/HOL/Algebra/More_Finite_Product.thy
changeset 67316 adaf279ce67b
parent 66760 d44ea023ac09
child 67341 df79ef3b3a41