src/HOL/Induct/SList.thy
changeset 46257 3ba3681d8930
parent 45694 4a8743618257
child 49834 b27bbb021df1