src/HOL/Tools/induct_method.ML
changeset 10910 058775a575db
parent 10871 0ff9caa810b1
child 11035 bad7568e76e0