src/HOL/Induct/SList.thy
changeset 11543 d61b913431c5
parent 11481 c77e5401f2ff
child 12169 d4ed9802082a