src/HOL/Induct/SList.thy
changeset 3257 4e3724e0659f
parent 3120 c58423c20740
child 3320 3a5e4930fb77
equal deleted inserted replaced
3256:0a45cdd7da37 3257:4e3724e0659f