src/HOL/Induct/SList.thy
changeset 30686 47a32dd1b86e
parent 30166 f47c812de07c
child 32960 69916a850301