src/HOL/Induct/SList.thy
changeset 36811 4ab4aa5bee1c
parent 35247 0831bd85eee5
child 39246 9e58f0499f57