src/HOL/Induct/SList.thy
changeset 79291 e9a788a75775
parent 67613 ce654b0e6d69
child 80914 d97fdabd9e2b
equal deleted inserted replaced
79290:9deadc9d8872 79291:e9a788a75775