src/HOL/Induct/SList.thy
changeset 12343 b05331869f79
parent 12169 d4ed9802082a
child 13079 e7738aa7267f