src/ZF/inductive.ML
changeset 5047 585fa380df1a
parent 516 1957113f0d7d