src/HOL/Induct/SList.ML
changeset 11083 d8fda557e476
parent 9747 043098ba5098
child 11500 a84130c7e6ab