src/HOL/Induct/Mutil.thy
changeset 8723 c7de3c2ed7a9
parent 8589 a24f7e5ee7ef
child 8781 d0c2bd57a9fb