src/HOL/Induct/SList.thy
changeset 8991 dc70b797827f
parent 6382 8b0c9205da75
child 11481 c77e5401f2ff
equal deleted inserted replaced
8990:19956dd3809e 8991:dc70b797827f