src/HOL/Induct/SList.thy
changeset 37950 bc285d91041e
parent 35247 0831bd85eee5
child 39246 9e58f0499f57