src/HOL/Tools/induct_tacs.ML
changeset 27187 17b63e145986
parent 27114 22e8c115f6c9
child 27215 b43785a81e01