src/ZF/Tools/induct_tacs.ML
changeset 16860 43abdba4da5c
parent 16458 4c6fd0c01d28
child 17057 0934ac31985f