src/HOL/Induct/SList.thy
changeset 33528 b34511bbc121
parent 32960 69916a850301