src/ZF/Tools/induct_tacs.ML
changeset 11145 3e47692e3a3e
parent 8438 b8389b4fca9c
child 12109 bd6eb9194a5d