src/ZF/inductive.thy
changeset 2319 95f0d5243c85
parent 124 858ab9a9b047