src/ZF/Inductive.thy
changeset 12720 f8a134b9a57f
parent 12372 cd3a09c7dac9
child 13259 01fa0c8dbc92