src/HOL/Induct/SList.thy
changeset 22815 d2b05f9462e0
parent 22267 ea31e6ea0e2e
child 23029 79ee75dc1e59