src/HOL/Induct/SList.thy
changeset 21086 fe9f43a1e5bd
parent 20820 58693343905f
child 21404 eb85850d3eb7