src/HOL/Induct/SList.thy
changeset 50210 747db833fbf7
parent 49834 b27bbb021df1
child 58112 8081087096ad