src/HOL/Induct/SList.thy
changeset 5089 f95e0a6eb775
parent 3842 b55686a7b22c
child 5191 8ceaa19f7717