src/ZF/Inductive.thy
changeset 12495 89f97fa683f5
parent 12372 cd3a09c7dac9
child 13259 01fa0c8dbc92
equal deleted inserted replaced
12494:58848edad3c4 12495:89f97fa683f5