src/HOL/Induct/SList.thy
changeset 82768 8f866fd6fae1
parent 81133 072cc2a92ba3