src/ZF/inductive.ML
changeset 5833 6d8bceaa07b3
parent 516 1957113f0d7d