src/HOL/Induct/SList.thy
changeset 30839 bf99ceb7d015
parent 30166 f47c812de07c
child 32960 69916a850301