src/HOL/Induct/SList.thy
changeset 81773 5df6481f45f9
parent 81133 072cc2a92ba3