src/HOL/Induct/SList.thy
changeset 21177 e8228486aa03
parent 20820 58693343905f
child 21404 eb85850d3eb7