src/HOL/Induct/SList.thy
changeset 61578 6623c81cb15a
parent 60530 44f9873d6f6f
child 61943 7fba644ed827