src/ZF/Tools/induct_tacs.ML
changeset 69826 1bea05713dde
parent 69593 3dda49e08b9d
child 70474 235396695401