src/HOL/Induct/SList.thy
changeset 37380 35815ce9218a
parent 35247 0831bd85eee5
child 39246 9e58f0499f57