src/HOL/Induct/Mutil.thy
changeset 9356 30c3d3e308ee
parent 8950 3e858b72fac9
child 9930 c02d48a47ed1