src/ZF/inductive.ML
changeset 777 c007eba368b7
parent 516 1957113f0d7d
equal deleted inserted replaced
776:df8f91c0e57c 777:c007eba368b7