src/HOL/Induct/SList.ML
changeset 10168 50be659d4222
parent 9747 043098ba5098
child 11500 a84130c7e6ab