src/ZF/inductive.thy
changeset 3257 4e3724e0659f
parent 124 858ab9a9b047
equal deleted inserted replaced
3256:0a45cdd7da37 3257:4e3724e0659f