src/ZF/Inductive.thy
changeset 777 c007eba368b7
parent 578 efc648d29dd0
child 805 96f51689cdeb
equal deleted inserted replaced
776:df8f91c0e57c 777:c007eba368b7