src/HOL/Induct/SList.ML
changeset 11838 02d75712061d
parent 11500 a84130c7e6ab
child 12169 d4ed9802082a