src/HOL/Induct/Mutil.thy
changeset 9714 79db0e5b7824
parent 8950 3e858b72fac9
child 9930 c02d48a47ed1