src/ZF/Inductive.thy
changeset 7760 43f8d28dbc6e
parent 6053 8a1059aa01f0
child 9491 1a36151ee2fc