src/HOL/Induct/SList.thy
changeset 60686 ea5bc46c11e6
parent 60530 44f9873d6f6f
child 61943 7fba644ed827