src/HOL/Induct/SList.ML
changeset 11701 3d51fbf81c17
parent 11500 a84130c7e6ab
child 12169 d4ed9802082a