src/ZF/Inductive.ML
changeset 798 31ec33d96231
parent 734 a3e0fd3c0f2f
child 802 2f2fbf0a7e4f