src/HOL/Induct/SList.thy
changeset 7990 0a604b2fc2b1
parent 6382 8b0c9205da75
child 11481 c77e5401f2ff