src/HOL/Induct/SList.thy
changeset 6105 b4ec1af7053f
parent 5977 9f0c8869cf71
child 6382 8b0c9205da75