src/HOL/Induct/SList.thy
changeset 5143 b94cd208f073
parent 3842 b55686a7b22c
child 5191 8ceaa19f7717