src/HOL/Induct/SList.thy
changeset 33621 dd564a26fd2f
parent 32960 69916a850301