src/HOL/Tools/induct_method.ML
changeset 7360 7d3136b9af08
parent 7017 e4e64a0b0b6b
child 7512 930e5947562d